量子科技中心_量科网

后量子密码（PQC）硬件掩码的形式化验证依赖于有限域上的SMT求解器。该团队先前工作实现了规模化结构依赖性分析[1]，并量化了部分NTT掩码的安全裕度[2]。其结构依赖性分析框架QANARY验证了Adams Bridge ML-DSA/ML-KEM加速器30个模块共计117万单元[3,4]，但核心可靠性结论（定理3.9.1）仅通过225个布尔线函数在q=5时完成机器验证。这使得向ML-KEM（q=3,329，FIPS 203[5]）和ML-DSA（q=8,380,417，FIPS 204[6]）的移植性成为未解难题。NIST IR 8547[7]（2025年3月）强调了填补此类空缺的重要性。研究人员首次给出定理3.9.1中r无关子定理的机器验证普适性证明：对于任意q>0、任意线函数及任意秘密对，值独立性蕴含边际分布一致性。该证明基于Lean 4[8]与Mathlib[9]实现，仅需5行代码即可替代225次有限域求值，且无需"sorry"占位符，将可信计算基从{Z3[10], CVC5[11], Python}缩减至Lean 4内核。该工作提出9条定理（T1-T6、T1'、T3'），涵盖重参数化、双射性、溢出边界、随机数生成器偏差，以及针对所有q≥2的普适非紧致反例。研究成果确立了ℤ/qℤ交换环公理作为算术掩码验证的自然抽象层。