💻 computer science

Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware

本文利用 Lean 4 形式化证明了在 ML-KEM/ML-DSA 硬件加速器中，采用每级新鲜掩码的流水线数论变换（NTT）在 ISW 一阶探测模型下满足安全性，并揭示了 Adams Bridge 加速器因掩码策略缺陷而存在结构性不安全。

原作者： Ray Iskander, Khaled Kirah

发布于 2026-04-23

📖 1 分钟阅读☕ 轻松阅读

原作者： Ray Iskander, Khaled Kirah

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

这篇论文主要解决了一个关于后量子密码学（PQC）硬件安全的“直觉陷阱”问题。为了让你轻松理解，我们可以把这篇论文的内容想象成**“如何安全地运送一箱贵重珠宝”**的故事。

1. 背景：运送珠宝的流水线

想象你是一家高科技公司的工程师，负责设计一条自动化流水线（NTT 流水线），用来运送极其珍贵的“数字珠宝”（加密密钥）。

任务：这条流水线由很多个加工站（蝴蝶单元，Butterfly Stages）串联而成。
挑战：路上有很多小偷（黑客），他们虽然不能直接偷走整箱珠宝，但可以在每个加工站偷偷看一眼（探测）其中一个零件。
传统防御（掩码技术）：为了防止被偷，工程师给每个零件都加了一层随机伪装（Masking）。比如，把真实的数字 $A$ 拆成 $A_{真实} + A_{随机}$ 。只要小偷只看一眼，看到的只是随机数，猜不出真实值。

2. 核心问题：直觉是错的！

以前的工程师有一个直觉：“只要每个加工站单独看都是安全的，那么整条流水线肯定也是安全的。”

以前的误区：工程师们认为，如果我在每个站都加了随机伪装，小偷就永远猜不到秘密。
这篇论文的发现：错！大错特错！
- 这就好比你给每个房间都上了锁，但如果房间之间的门没锁，小偷可以从一个房间溜到另一个房间，把线索拼凑起来。
- 论文发现，如果只在第一个房间（第一站）加了随机伪装，而后面的房间（后续站）直接传递数据不加新的伪装，小偷就能通过观察不同房间的数据变化，像拼图一样还原出秘密。
- 著名的“亚当斯桥”（Adams Bridge）案例：论文指出，一个名为“亚当斯桥”的著名硬件设计，就犯了这个错误。它只在第一站加了伪装，后面几站直接裸奔。之前的研究只是发现了它不安全，但这篇论文从数学上证明了为什么它不安全——因为它违反了“每站都要换新伪装”的原则。

3. 三个关键发现（用比喻解释）

发现一：填补了“随机性”的数学空白

比喻：以前数学家证明了“如果锁是好的，门就是安全的”，但没证明“如果锁是随机换的，门是不是还安全”。
论文贡献：作者用计算机（Lean 4 证明助手）严格证明了：只要每次换锁用的钥匙是全新的、随机的，那么无论小偷怎么观察，都绝对无法推断出里面的秘密。这填补了之前理论的一个小缺口。

发现二：揭穿了一个“假警报”陷阱

比喻：有些工程师会检查：“如果我不换钥匙，小偷看到的数字变不变？”如果变了，他们就以为系统不安全，于是把正确的设计也扔掉了。
论文贡献：作者证明，对于这种特殊的“蝴蝶”加工站，“不换钥匙数字会变”是正常的（就像你往杯子里倒水，水位肯定会变，但这不代表杯子漏水）。
警示：这是一个**“假警报”**。如果工程师用这个标准去检查，会误杀所有安全的设计。论文给这个陷阱起了个名字，警告大家不要掉进这个坑。

发现三：证明了“新鲜伪装”是万能钥匙

比喻：这是论文最核心的结论。作者证明了：只要每一个加工站在传递数据时，都重新加上一层全新的、随机的伪装（Fresh Masking），那么无论流水线有多长（100 个站还是 1000 个站），小偷都绝对无法拼凑出秘密。
数学意义：这就像给每个房间都换了一把全新的、互不相关的锁。小偷就算在每个房间都偷看一眼，看到的也是完全随机的乱码，永远连不成线。
结果：这个结论是机器自动验证的（由计算机代码严格证明，没有人为疏漏），适用于所有类型的后量子密码算法。

4. 为什么这很重要？

给硬件工程师的“定心丸”：以前大家凭直觉设计，现在有了机器证明的“安全证书”。只要遵循“每站换新伪装”的原则，就可以自信地告诉监管机构（如 NIST）：我的硬件是安全的。
给监管机构的“证据”：在 FIPS（美国联邦信息处理标准）认证中，现在可以直接引用这篇论文的机器证明结果，证明设计是安全的。
指出了“亚当斯桥”的病灶：它明确告诉业界，那个著名的设计之所以不安全，不是因为它算错了，而是因为它偷懒了（只在第一站加了伪装，后面没加）。

5. 总结

这篇论文就像是一位**“数学侦探”**，做了一件三件事：

补全了理论：证明了“随机换锁”确实能保护整条流水线。
排除了干扰：告诉工程师别被“假警报”吓跑，有些变化是正常的。
立下了规矩：提出了**“新鲜伪装设计原则”**——每经过一个加工站，必须换一次全新的随机伪装。

只要遵守这个原则，后量子密码的硬件就能像铜墙铁壁一样，抵御小偷的窥探。而如果不遵守（像“亚当斯桥”那样），再好的设计也会像漏水的桶一样，被黑客轻易攻破。

一句话总结：这篇论文用计算机严格证明了，在后量子密码硬件中，**“每走一步都要换一次新伪装”**是保证绝对安全的唯一真理。

这是一份关于论文《Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware》（新鲜掩码使 NTT 流水线可组合：PQC 硬件中算术掩码的机器检查证明）的详细技术总结。

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

背景：
后量子密码学（PQC）加速器（如符合 FIPS 203 ML-KEM 和 FIPS 204 ML-DSA 标准的硬件）广泛依赖数论变换（NTT）流水线。为了抵御侧信道攻击（如功耗分析），这些硬件通常采用一阶算术掩码（Arithmetic Masking）技术，将秘密值 $s$ 拆分为 $s_0 + s_1 \pmod q$ 。

核心问题：
尽管现有的掩码组合框架（如 ISW、t-SNI、PINI、DOM）在理论上适用于任意环，但它们的机器检查（Machine-Checked）形式化验证和工具实现主要针对布尔电路（$GF(2)$）。

缺乏算术掩码的组合性证明： 对于在 $\mathbb{Z}_q$ 上运行的 NTT 蝴蝶（Butterfly）结构，是否存在机器检查过的证明，表明“每一级单独安全”能推导出“整个流水线安全”？此前没有答案。
设计直觉的陷阱： 硬件工程师常直觉认为“如果每一级都安全，流水线就安全”。然而，对于 NTT 蝴蝶输出，一种直观的验证属性（逐点值独立性，Pointwise Value-Independence）实际上是错误的。如果设计师使用 SMT 求解器检查此属性，会错误地判定正确的设计为“不安全”。
实际案例的隐患： 现有的 Adams Bridge 加速器（CHIPS Alliance Caliptra 项目的一部分）在 NTT 流水线中仅在初始轮次使用掩码，后续轮次未注入新鲜随机掩码。之前的实证分析（Paper 1 & 2）发现了其安全性不足，但缺乏理论上的根本原因解释。

2. 方法论 (Methodology)

本文采用形式化验证方法，使用 Lean 4 定理证明器和 Mathlib 库，对 NTT 流水线中的算术掩码进行了严格的机器检查证明。

形式化模型：
- 定义了在 $\mathbb{Z}_q$ （ $q > 0$ ，不一定是素数）上的 Cooley-Tukey 蝴蝶运算。
- 采用 ISW 一阶探测模型（First-order Probing Model）：攻击者每个时钟周期只能观察一条线。
- 引入“新鲜掩码”（Fresh Masking）假设：每一级流水线都使用独立采样的新鲜随机掩码。
核心逻辑：
- 利用 NTT 蝴蝶运算在掩码上的仿射性质（Affine Property）。与布尔掩码中的非线性与门（AND）不同，NTT 蝴蝶类似于布尔掩码中的异或（XOR），是线性的。
- 证明了在新鲜掩码下，输出值的分布关于掩码是均匀的（Uniform），且独立于秘密值。
验证规模：
- 包含 9 个主要定理。
- 构建作业 1,738 次，零错误（Zero sorry），完全形式化。

3. 关键贡献 (Key Contributions)

本文提出了三个主要的机器检查证明结果：

A. 填补理论缺口：r-bearing 桥接 (The r-Bearing Bridge)

内容： 解决了作者先前工作（Paper 3）中的一个明确限制。证明了在引入新鲜随机性（fresh randomness）后，“值独立性”（Value-Independence）依然蕴含“边际分布恒定”（Constant Marginal Distribution）。
意义： 建立了从代数性质到信息论性质（互信息 $I(x; w) = 0$ ）的严格桥梁，通过代数代理 MutualInfoZero 实现。

B. 纠正设计陷阱：蝴蝶每上下文均匀性 (Butterfly Per-Context Uniformity)

发现陷阱： 证明了逐点值独立性（Pointwise Value-Independence）对于蝴蝶输出是假的。如果固定掩码，改变秘密输入，输出线值确实会改变。这是一个常见的验证陷阱。
确立正确属性： 证明了边际均匀性（Marginal Uniformity）。即：对于任意输出值 $v$ ，恰好存在唯一的一个掩码值 $m$ 使得输出为 $v$ 。
普适性： 该证明对所有 $q > 0$ 、所有旋转因子（Twiddle factors）和所有输入均成立。这意味着无论模数是多少（如 ML-KEM 的 3329 或 ML-DSA 的 8380417），只要使用新鲜掩码，该属性就成立。

C. 流水线组合性证明 (Pipeline Composition)

核心定理： 证明了具有新鲜每级掩码的 $k$ 级 NTT 流水线，在每一级都满足“每上下文均匀性”。
机制： 利用数学归纳法，结合“状态更新不影响未来”的引理，证明每一级的输出分布仅依赖于该级的新鲜掩码，且独立于之前的秘密状态。
结论： 只要每一级注入新鲜掩码，整个流水线就是一阶探测安全的。

4. 主要结果 (Results)

理论验证： 首次提供了针对 $\mathbb{Z}_q$ 上 NTT 蝴蝶结构的机器检查组合性证明。
设计原则确立： 提出了**“新鲜掩码设计原则”（Fresh Masking Design Principle）**：NTT 流水线要实现一阶探测安全，必须在每一级 Cooley-Tukey 蝴蝶阶段注入独立的新鲜掩码。
Adams Bridge 失效原因解析：
- Adams Bridge 加速器仅在 INTT 第 0 轮使用掩码，后续轮次未更新掩码。
- 本文证明指出，由于违反了“新鲜掩码”假设，流水线组合定理的前提条件不满足，因此其安全性无法得到保证。这从架构根源上解释了为何该设计存在结构性不安全（与 Paper 1 & 2 的实证分析一致）。
非线性扩展预告： 指出 NTT 蝴蝶是线性情况（类似 XOR），而 Barrett 约减等非线性组件（类似 AND）需要不同的证明框架（将在后续论文 [3] 中通过 PF-PINI 框架解决）。

5. 意义与影响 (Significance)

对硬件设计者的指导： 为 PQC 硬件工程师提供了明确的验证指南。设计师不再需要盲目猜测，而是可以依据机器检查的证明来设计流水线，避免陷入“逐点值独立性”的验证陷阱。
FIPS 认证支持： 为 NIST FIPS 140-3 认证提供了强有力的证据。该证明是机器检查的、普遍量化的，可直接作为侧信道抗性（Side-Channel Resistance）的数学证据提交给评估机构。
填补领域空白： 填补了现有形式化验证工具（如 SILVER, maskVerif 等）仅针对布尔电路的空白，将形式化验证扩展到了 PQC 核心的算术 NTT 领域。
通用性： 证明不依赖于特定的模数 $q$ 是否为素数，适用于所有 PQC 标准及未来可能的新标准。

总结

这篇文章通过 Lean 4 形式化验证，解决了 PQC 硬件中算术掩码组合性的关键理论缺失。它证明了新鲜掩码是 NTT 流水线安全组合的充分条件，并揭示了现有设计（如 Adams Bridge）因违反此原则而存在的安全隐患。这项工作为构建可证明安全的后量子密码硬件加速器奠定了坚实的数学和形式化基础。