Post-quantum cryptographic (PQC) accelerators implementing ML-KEM (FIPS 203) and ML-DSA (FIPS 204) require side-channel resistance evidence for FIPS 140-3 certification. However, exact masking-verification tools scale only to gadgets of a few thousand cells. We present a four-stage verification hierarchy, D0/D1 structural dependency analysis, fresh-mask refinement, Boolean Single-Authentication Distance Checking (SADC), and arithmetic SADC, that extends sound first-order masking verification to production arithmetic modules. Applied to the 1.17-million-cell Adams Bridge ML-DSA/ML-KEM accelerator, structural analysis completes in seconds across all 30 masked submodules. A multi-cycle extension (MC-D1) reclassifies 12 modules from structurally clean to structurally flagged. On the 5,543-cell ML-KEM Barrett reduction module, the pipeline machine-verifies 198 of 363 structurally flagged wires (54.5%) as first-order secure, reports 165 as candidate insecure for designer triage (a sound upper bound), and leaves 0 indeterminate. Every verdict is cross validated by Z3 and CVC5 with 0 disagreements across 363 wires. The result narrows manual review from hundreds of structural flags to 165 actionable candidates with mathematical certificates, enabling pre-silicon side-channel evidence generation on production ML-KEM hardware.

翻译：实现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个模块从结构清洁重新归类为结构标记。在5,543单元的ML-KEM Barrett约简模块上，该流水线可自动验证363条结构标记线中的198条（54.5%）为一阶安全，将165条标记为候选不安全供设计人员排查（可靠上界），且不产生任何不确定判定。所有结论均通过Z3和CVC5交叉验证，363条线路上无任何分歧。该结果将人工审查范围从数百条结构标记缩减至165个具有数学证明的可操作候选对象，从而在生产级ML-KEM硬件上实现硅前侧信道证据生成。