💻 computer science

From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification

本文利用 Lean 4 形式化验证系统，将后量子密码硬件掩码安全性验证从依赖有限枚举的 SMT 求解方法，提升为基于 $\mathbb{Z}/q\mathbb{Z}$ 交换环公理的通用数学证明，从而消除了从特定小模数到 NIST 标准大模数（如 ML-KEM/ML-DSA）验证的鸿沟并显著缩小了可信计算基。

原作者： Ray Iskander, Khaled Kirah

发布于 2026-04-22

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Ray Iskander, Khaled Kirah

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇论文讲述了一个关于**“如何给未来的超级电脑（抗量子密码）穿上防弹衣”**的数学故事。

为了让你轻松理解，我们可以把这篇论文里的技术概念想象成一场**“密码锁与万能钥匙”**的冒险。

1. 背景：未来的密码锁与现在的“试错法”

想象一下，我们即将进入一个由“后量子密码”（PQC）保护的新世界。这些密码锁非常复杂，就像是一个巨大的、由数字组成的迷宫（数学上叫“有限域”或 $\mathbb{Z}_q$ ）。

为了防止黑客通过观察电脑耗电量的微小变化（侧信道攻击）来猜出密码，工程师们给这些密码锁加了一层“防弹衣”，叫做**“掩码”（Masking）**。

通俗解释：这就好比把秘密数字 $x$ 拆成两半， $s_0$ 和 $s_1$ ，只有把它们加起来（模 $q$ ）才是真密码。黑客只能看到其中一半，所以什么都猜不到。

过去的问题（Paper 2 的工作）：
以前的团队（QANARY 框架）开发了一个超级聪明的“安检员”（SMT 求解器），用来检查这些防弹衣有没有漏洞。

之前的做法：这个安检员很勤奋，但它有点“笨”。它只能在一个很小的数字世界里（比如 $q=5$ ，只有 0,1,2,3,4 这五个数字）进行穷举测试。它把 225 种可能的情况全部跑了一遍，发现：“嘿，在这个小世界里，防弹衣是完美的！”
隐患：但是，真正的密码锁用的数字世界大得惊人（比如 $q=3329$ $q = 3329$ 或 $q=8,380,417$ $q = 8, 380, 417$ ）。
- 比喻：这就像你为了证明“所有天鹅都是白的”，只在自家后院（ $q=5$ ）数了 225 只天鹅。虽然后院的天鹅都是白的，但你不能保证在遥远的南极（ $q=3329$ ）没有黑天鹅。之前的证明在数学上是不完整的，因为“小世界”的规律不一定适用于“大世界”。

2. 突破：从“数数”到“理解原理”

这篇论文（Paper 3）做了一件惊天动地的事：他们不再数数了，而是直接证明了原理。

作者 Ray Iskander 和 Khaled Kirah 使用了一种叫 Lean 4 的“数学证明助手”（交互式定理证明器），写了一个只有5 行代码的证明。

之前的 225 次测试：像是在问：“如果 $q=5$ ，行不行？如果 $q=6$ ，行不行？……"
现在的 5 行证明：像是直接说：“因为加法交换律和减法消去律（环论公理）是宇宙通用的真理，所以无论 $q$ 是 5 还是 800 万，只要防弹衣的设计符合这些数学规则，它就永远是安全的。”

核心比喻：从“试钥匙”到“看图纸”

旧方法（SMT 求解器）：像是一个拿着 225 把不同形状钥匙的锁匠，一把一把地试，发现都能打开。但他不敢保证第 226 把钥匙也能打开。
新方法（Lean 4 证明）：像是一个建筑大师，直接指着锁的设计图纸说：“看，这个锁的结构是基于‘圆环’原理设计的。只要它是圆环，无论它转多大，结构都不会散架。”
- 这 5 行代码证明了：“价值独立性”（Value-Independence）意味着“分布恒定”。简单说，就是只要你的防弹衣设计得让黑客看不出秘密数字的痕迹，那么无论数字多大，这个性质都自动成立。

3. 为什么这很重要？（9 个定理的“全家福”）

除了那个核心的 5 行证明，他们还写了 9 个定理（T1-T6 等），就像给这个新理论盖了 9 个印章：

通用性：不管 $q$ 是多少（只要大于 0），证明都有效。
无漏洞：之前的证明依赖复杂的软件（Z3/CVC5），万一软件有 Bug 怎么办？现在的证明直接由 Lean 4 的“核心引擎”验证，就像由最严谨的数学公理直接背书，零错误（Sorry-free）。
甚至指出了“保守”的必要性：他们发现，有些情况虽然看起来安全，但为了绝对保险，系统会故意把它们标记为“不安全”。这就像安检员宁可错杀一千，不可放过一个。论文证明了这种“多疑”是合理的，不是系统故障。

4. 对现实世界的影响

对 NIST（美国国家标准与技术研究院）：以前，每换一个密码标准（比如从 ML-KEM 换到 ML-DSA），就要重新跑一遍那 225 次测试，甚至要担心新的大数字会不会出问题。现在，一次证明，永久有效。无论未来 NIST 选多大的数字，这个数学证明都覆盖到了。
对硬件工程师：他们可以放心地设计芯片，因为背后的数学基础已经从“经验主义”（试出来的）变成了“绝对真理”（证出来的）。
对信任：以前我们信任的是“那个跑测试的软件没 Bug"；现在我们信任的是“数学公理本身”。这就像从“相信天气预报”变成了“相信万有引力”。

总结

这篇论文就像是在说：

“我们以前为了证明‘所有天鹅都是白的’，在池塘边数了 225 只天鹅。现在，我们直接证明了‘天鹅的基因决定了它只能是白的’。无论池塘大小，无论时间流逝，这个结论永远成立。”

他们用5 行代码，取代了3300 万次计算，把后量子密码硬件的安全性，从“大概率正确”提升到了“数学上绝对正确”。这就是从“有限枚举”到“通用证明”的飞跃。

这篇论文《从有限枚举到通用证明：PQC 硬件掩码验证的环论基础》（From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification）由 Ray Iskander 和 Khaled Kirah 撰写，旨在解决后量子密码（PQC）硬件实现中侧信道攻击防护形式化验证的关键缺口。

以下是该论文的详细技术总结：

1. 研究背景与问题 (Problem)

背景：随着 NIST 标准化 ML-KEM (FIPS 203) 和 ML-DSA (FIPS 204)，大规模向 PQC 迁移正在进行。硬件加速器（如 Adams Bridge）通常使用数论变换（NTT）和算术掩码（Arithmetic Masking）来防御功耗侧信道攻击。
现有方法的局限性：
- 先前的工作（QANARY 框架）使用 SMT 求解器（Z3, CVC5）在有限域（模数 $q=5$ ）上对 1.17 百万个单元进行了结构依赖分析。
- 核心缺陷：SMT 求解器基于枚举（Enumeration），无法进行结构归纳（Structural Induction）。在 $q=5$ 时的验证结果不能逻辑上保证在真实生产参数（如 ML-KEM 的 $q=3,329$ 或 ML-DSA 的 $q=8,380,417$ ）下依然成立。
- 信任基问题：现有方法依赖于复杂的 SMT 求解器和 Python 编码，缺乏形式化验证的“最小信任基”。
待解决问题：如何证明“值独立性（Value-Independence）”这一属性在所有模数 $q > 0$ 下都能保证掩码后的信号不泄露秘密信息，从而填补从有限域验证到通用数学证明的鸿沟。

2. 方法论 (Methodology)

工具选择：采用 Lean 4 交互式定理证明器及其数学库 Mathlib。
核心抽象：将算术掩码验证的底层逻辑从“位向量（Bit-vector）”和“布尔可满足性（SAT）”转移到**交换环（Commutative Ring）**代数结构上。
- 利用 Mathlib 中的 ZMod q 类型，直接表示商环 $\mathbb{Z}/q\mathbb{Z}$ 。
- 利用环的公理（如 sub_add_cancel）来处理模运算，避免了位向量编码中繁琐的溢出检查和显式模运算。
验证策略：
- 不再枚举所有可能的输入组合（这在 $q$ 很大时是不可行的）。
- 通过结构归纳和代数重写，证明对于任意 $q$ 、任意线函数 $w$ 和任意秘密 $x$ ，如果满足值独立性，则其边际分布是恒定的。
- 所有证明均为 sorry-free（无未验证的存根），完全由 Lean 内核验证。

3. 关键贡献 (Key Contributions)

论文提出了一个完整的机器验证证明套件，包含 9 个定理（T1–T6, T1', T3'），主要贡献如下：

通用主定理（Theorem 4.1）：
- 证明了对于任意 $q>0$ ，如果线函数 $w$ 是值独立的（即 $w(x-s_1, s_1) = w(x'-s_1, s_1)$ ），那么其边际分布（Marginal Distribution）是常数。
- 证明长度：仅需 5 行 Lean 代码。相比之下，之前的 SMT 方法需要枚举 $225 $个布尔函数（在$ q=5$ 时），且无法推广。
- 意义：确立了 $\mathbb{Z}/q\mathbb{Z}$ 的交换环公理是算术掩码验证的自然抽象层。
支持性定理套件：
- T2 & T3：证明了布尔和算术重参数化（Reparametrization）的往返性质（Round-trip），即 $(x \oplus s) \oplus s = x$ 和 $(x - s) + s = x$ 。在 Lean 中，这直接由环公理得出，无需溢出检查。
- T3'：证明了重参数化映射的双射性（Bijectivity），确保掩码覆盖整个空间。
- T4：建立了无溢出边界，桥接了抽象环理论与实际硬件位向量实现。
- T5：量化了随机数生成器（RNG）的偏差，并提供了通用边界证明。
- T6：提供了一个通用反例，证明“边际分布恒定”并不蕴含“值独立性”（即定理的逆命题不成立），从而解释了 QANARY 分析中保守性（Conservative）判定的必要性。
方法论洞察：
- 揭示了之前的 SMT 方法之所以复杂，是因为在错误的形式化（位向量 SAT）中工作。
- 证明了代数结构（环论）能极大地简化验证过程，使证明从“计算密集型”转变为“逻辑推导型”。

4. 实验结果 (Results)

验证规模：整个证明套件包含 1,739 个构建任务，0 个 sorry，0 个错误。
效率对比：
- 之前：在 $q=5$ 时，Z3/CVC5 需要检查 $33,554,432 $个布尔线函数实例（$ 225 $个函数$ \times$ 输入组合）。
- 现在：Lean 4 仅需 5 行代码即可证明对所有 $q$ 成立。
覆盖范围：证明覆盖了所有 $q>0$ 的情况，包括 ML-KEM ( $q=3,329$ ) 和 ML-DSA ( $q=8,380,417$ )，以及未来任何 NIST PQC 标准。
代码可用性：所有代码已开源（GitHub 和 Zenodo），使用 Lean 4.30.0-rc1 和 Mathlib 特定提交版本。

5. 意义与影响 (Significance)

消除验证缺口：彻底解决了 QANARY 框架中“有限域验证无法推广到生产参数”的方法论缺陷。
降低认证负担：对于 FIPS 140-3 认证，不再需要针对每个参数集（ $q$ 值）重新进行验证。一次通用的机器验证即可覆盖所有现存的和未来可能的 PQC 参数集。
提升工具信任度：将信任基（Trusted Base）从庞大的、未经验证的 SMT 求解器（Z3/CVC5）缩小到极简的、经过形式化规范的 Lean 4 内核。
范式转变：证明了环论是算术掩码验证的自然语言。这一发现可能启发其他复杂属性（如高阶掩码、混合布尔 - 算术转换）的简洁证明。
安全性保证：确认了 QANARY 之前的“保守性”判定（将某些线标记为 INSECURE_CONSERVATIVE）是数学上不可避免的，而非工具实现的缺陷，从而增强了安全评估的可信度。

总结：
该论文通过将 PQC 硬件掩码验证从基于枚举的 SMT 方法转变为基于代数结构的交互式定理证明，实现了从“特定实例验证”到“通用数学证明”的飞跃。这不仅解决了当前 PQC 硬件安全验证的关键瓶颈，也为未来的形式化验证工作确立了新的代数抽象标准。