量子科技中心_量科网

实施ML-KEM（FIPS 203）和ML-DSA（FIPS 204）的后量子密码（PQC）加速器需要提供抗旁道攻击证据以获得FIPS 140-3认证。然而现有掩码验证工具仅能处理数千单元规模的模块。该团队提出四阶段验证体系：D0/D1结构依赖性分析、新掩码优化、布尔型单认证距离检查（SADC）及算术型SADC，将可靠的一阶掩码验证扩展到实际运算模块。在包含117万个单元的Adams Bridge ML-DSA/ML-KEM加速器测试中，结构分析仅用数秒便完成全部30个掩码子模块检测。通过多周期扩展方法（MC-D1），12个模块从"结构清洁"状态被重新标记为"需核查"。针对含5543个单元的ML-KEM Barrett约减模块，验证流程自动判定363条结构标记线中的198条（54.5%）具备一阶安全性，将165条列为需设计者复核的潜在风险线（可靠上界），剩余0条未定状态。所有结论均经Z3和CVC5交叉验证，363条线判定结果完全一致。该方法将人工核查范围从数百条结构标记线缩减至165条可溯源的候选线，为量产级ML-KEM硬件提供了流片前的旁道攻击防护证据。