💻 computer science

Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking

本文提出了首个针对素域算术掩码的机器验证组合定理，证明了流水线级间引入新鲜随机掩码可确保安全性独立于先前阶段，并利用这些形式化结果诊断出微软 Adams Bridge 后量子密码加速器中存在的关键级间掩码缺陷。

原作者： Ray Iskander, Khaled Kirah

发布于 2026-04-29

📖 1 分钟阅读☕ 轻松阅读

原作者： Ray Iskander, Khaled Kirah

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

想象一下，你正试图通过一条工厂装配线发送一条秘密消息。这条消息非常敏感，因此你不希望任何监视生产线的人能够猜出它的内容。为了保护它，你在消息进入下一站之前，将其拆分成若干片段，并将每个片段与随机的“噪声”（即掩码）混合。这被称为掩蔽。

在计算机安全领域，主要有两种类型的噪声：

布尔噪声：就像翻转开关（开/关）。我们早已拥有一套完美的规则手册，指导如何安全地堆叠这些开关。
算术噪声：就像在时钟上相加数字（其中 12 + 1 = 1）。这正是现代“后量子”密码学所使用的。直到如今，我们还没有一套规则手册来指导如何安全地堆叠这些基于数字的掩码。

本文提供了那本缺失的规则手册。以下是他们发现的故事，以简单的方式解释。

1. 问题：“泄漏”的中间环节

想象一条两步工厂生产线：

站点 A：接收你的秘密，添加一些噪声，然后将其传递下去。
站点 B：接收站点 A 传递的内容，添加更多噪声，然后发送最终结果。

研究人员发现，在连接这些站点的方式中存在一个危险的缺陷，该缺陷出现在一款著名的微软安全芯片（称为"Adams Bridge"）中。

在这种有缺陷的设计中，站点 A 将其带噪声的结果直接传递给站点 B。由于数学运算的方式（具体来说是称为"Barrett 约减”的步骤，这是一种复杂的除法方式），从站点 A 输出的“噪声”并非完全随机。它存在某种模式。

类比：想象站点 A 是一台搅拌机。它将你的秘密与冰块混合。但由于刀片旋转的方式，出来的冰块块状物略有不均——有些地方的冰块多，有些地方的冰块少。如果一名间谍（黑客）站在站点 A 和站点 B 之间并清点冰块块数，他们就能猜出你秘密的一部分。这被称为侧信道攻击。

2. 解决方案：“新鲜掩码”（更新论证）

这篇论文的“顿悟”时刻出奇地简单。他们证明，如果在站点 A 和站点 B 之间插入一个全新的、随机的掩码，问题会瞬间消失。

类比：

未修复时：站点 A 将一堆略有不均的冰块交给站点 B。站点 B 试图修复它，但不均匀性已经内嵌其中。
修复后：站点 A 将其不均匀的冰块堆交给一个“重置按钮”。该按钮将冰块堆倒入一个巨大的、完全混合的新鲜水桶中（即新掩码）。现在，当站点 B 从这个桶中舀取一勺时，它又变得完全随机了。

论文从数学上证明，这个新鲜掩码完全擦除了站点 A 的记忆。无论站点 A 是混乱还是完美，一旦应用了新鲜掩码，连接到站点 B 的线路就变得完全均匀。整个生产线的安全性现在仅取决于站点 B 的优劣。

3. "1 比特障碍”

研究人员发现，对于这些芯片所使用的特定数学运算（Barrett 约减），噪声本身永远无法做到完全随机。它存在高达 1 比特信息的“泄漏”。

这就像一枚略微偏重的硬币。它不是公平的硬币；它落在“正面”的频率略高。
这并非设计失误，而是数学的根本属性。论文将此称为**"1 比特障碍”**。
然而，论文证明，如果你在阶段之间使用“新鲜掩码”技巧，那 1 比特的泄漏就会被隐藏在新鲜噪声中，对间谍变得毫无用处。

4. 证明：机器验证

作者们不仅仅是在纸上写下这些内容；他们使用了一个名为Lean 4的计算机程序来检查他们逻辑中的每一步。

他们撰写了 18 个具体的证明。
计算机以零错误和零“稍后处理”注释（称为"sorry stubs"）验证了所有这些证明。
这意味着数学基础坚如磐石。这不仅仅是一个理论；它是一个经过验证的事实。

5. 诊断：微软芯片为何易受攻击

该团队将他们的新规则手册应用于微软的"Adams Bridge"芯片。

发现：该芯片包含两个阶段（Butterfly 和 Barrett），但两者之间没有新鲜掩码。
结果：连接这两个阶段的线路是“泄漏”的。它并不均匀。这证实了为何其他研究人员已经成功利用功耗分析（测量电力消耗）破解了该芯片。
修复方案：论文提出了一种简单的修复方法：在阶段之间添加一个额外的随机数生成器和一个减法步骤。这使得中间线路变得完全安全。

总结

本文解决了安全计算机芯片拼图中的缺失部分。

问题：当将数学运算串联在一起时，用于隐藏秘密的“噪声”可能在中间变得混乱并泄露信息。
修复：在每一步之间插入一个全新的随机“重置”。
证明：他们使用计算机证明，这种重置使得中间线路完全安全，无论第一步多么混乱。
应用：他们确切地展示了一款著名的微软芯片为何存在漏洞，以及如何通过简单的架构更改来修复它。

简而言之：如果你希望通过多步骤过程隐藏秘密，不要仅仅依赖第一步的伪装。在每一步之间都加入一个新的伪装，秘密就能保持安全。

以下是论文《素域 PINI：后量子 NTT 掩码的机器验证组合定理》的详细技术总结。

1. 问题陈述

本文解决了后量子密码学（PQC）硬件形式化安全验证中的一个关键缺口，特别是针对 NIST 标准（ML-KEM 和 ML-DSA）中使用的数论变换（NTT）实现。

背景：NTT 的硬件实现依赖于素域（ $\mathbb{Z}_q$ ）上的算术掩码，以抵御差分功耗分析（DPA）等侧信道攻击。
缺口：虽然布尔掩码（在 $GF(2^n)$ 上）已拥有成熟的组合理论（NI、SNI、PINI）及机器验证证明，但素域上的算术掩码缺乏类似的组合定理。
具体问题：在算术掩码中，模约减等操作（如 Barrett 约减）会以非平凡的方式与掩码相互作用。与完美保持均匀性的布尔异或（XOR）不同，算术掩码可能导致输出分布不均匀（多重性 > 1）。
漏洞：先前的实证分析和结构研究指出了微软"Adams Bridge"PQC 加速器中的漏洞，其中流水线级之间的中间信号线不均匀，从而允许 DPA 攻击。然而，此前缺乏关于为何会发生这种情况以及如何通过组合定理来解决这一问题的形式化理论解释。

2. 方法论

作者利用Lean 4证明助手进行形式化验证，推导并证明了算术掩码的组合定理。

形式化模型：他们定义了一个名为PF-PINI(k)（素域探针隔离非干扰）的定量安全指标。
- 与二元安全概念（安全/不安全）不同，PF-PINI 衡量输出值相对于掩码空间的多重性。
- $k=1$ 意味着完美均匀分布。
- $k=2$ 意味着最大多重性为 2，每条信号线最多泄露 1 比特信息。
“更新论证”：核心理论见解是，在两个流水线级之间应用新鲜随机掩码会完全“擦除”第一级的安全参数（ $k_1$ ），无论第一级的输出多么不均匀，中间信号线都会恢复均匀。
硬件桥接：作者形式化地 bridged 了抽象代数模型（ $\mathbb{Z}_q$ ）与 RTL 设计中使用的硬件忠实自然数算术（Nat）之间的差距，特别是针对 Barrett 约减。
验证范围：整个工作包含18 个机器验证定理，且零 sorry 存根（无未证明假设），确保了高保障保证。

3. 主要贡献

本文做出了六项主要贡献：

更新定理（定理 4.1）：证明如果在两个级（ $G_1 \to G_2$ ）之间应用新鲜随机掩码，中间信号线将变得完美均匀。产生任何特定中间值的掩码对集合的基数恰好为 $q$ ，与 $G_1$ 的安全参数无关。
正组合定理（定理 4.4）：证明带有新鲜掩码的两级流水线满足PF-PINI( $k_2$ )。组合输出的安全性仅取决于第二级的参数（ $k_2$ ）；第一级的弱点（ $k_1$ ）被完全擦除。
负组合定理（定理 5.1–5.3）：证明若无新鲜掩码，中间信号线将保留第一级的多重性（ $k_1$ ）。如果 $k_1 > 1$ ，信号线将不均匀，这是 DPA 攻击的必要条件。
代数 - 硬件桥接（定理 6.1）：形式化证明在标准范围条件（ $q \le 2^s$ ）下，代数 Barrett 约减映射等价于硬件忠实的 Nat 算术映射。这验证了理论界限直接适用于硅片实现。
Adams Bridge 诊断：形式化实例化定理以诊断微软的 Adams Bridge 加速器。证明确认，缺乏级间新鲜掩码导致 Barrett 输出信号线不均匀（PF-PINI(2)），这解释了先前实证 DPA 攻击成功的原因。
通用 1 比特屏障：提供了计算证据，表明 PF-PINI(2) 界限对于模约减（包括 Barrett 和 Montgomery）是通用的，暗示这些操作存在根本性的"1 比特屏障”。

4. 关键结果

组合的形式化证明：本文确立了级间新鲜掩码是安全组合算术组件的必要且充分条件。
定量安全：
- 有新鲜掩码：中间信号线是均匀的（ $k=1$ ）。最终输出受第二级参数（ $k_2$ ）限制。
- 无新鲜掩码：中间信号线不均匀（高达 $k_1$ ）。这种不均匀性是实证攻击中观察到的侧信道泄露的根本原因。
Adams Bridge 修复：诊断确认，在 Adams Bridge 流水线的 Butterfly 和 Barrett 级之间添加单个新鲜随机掩码寄存器和减法操作，将消除中间信号线上的 DPA 漏洞，且不改变最终输出安全参数。
工件可用性：完整的 Lean 4 源代码（包括 18 个定理和复现脚本）已公开，允许独立验证证明。

5. 意义

首个机器验证的算术组合：这是首个为素域上的算术掩码提供机器验证组合定理的工作，填补了 PQC 硬件安全领域的主要理论空白。
** bridging 理论与实践**：通过将抽象代数证明与硬件忠实算术形式化地联系起来，本文为验证现实世界的硅片设计提供了严谨的基础，超越了实证测试。
设计指南：它为 PQC 硬件确立了一条清晰、可证明的设计规则：始终在流水线级之间插入新鲜掩码。这一简单的架构变更保证了组合流水线的安全性仅由最后一级中最薄弱的环节决定，而非中间级。
证据汇聚：形式化证明与三项独立的先前分析（实证功耗分析、代码审查和结构依赖分析）完美吻合，确认了 Adams Bridge 加速器中识别出的架构缺陷确实是其漏洞的根本原因。

总之，本文提供了设计安全、可组合且抗侧信道攻击的后量子密码学新时代硬件加速器所需的数学和形式化验证骨干。