💻 computer science

The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware

本文提出了一项在 Lean 4 中经机器验证的证明，该证明表明，通过推广先前的组合定理并验证蒙哥马利约化性质，具有新鲜级间掩码和 PF-PINI( $\leq 2$ ) 组件的任意深度 $k$ 级掩码 NTT 流水线可实现与流水线深度无关的 $2/q$ 通用单次观测泄露上界。

原作者： Ray Iskander, Khaled Kirah

发布于 2026-05-07

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Ray Iskander, Khaled Kirah

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

以下是用通俗语言和创意类比对论文《1 比特屏障具有普适性》的解释。

宏观图景：在嘈杂工厂中保护秘密

想象你经营着一家高安全级别的工厂，负责处理绝密蓝图（加密密钥）。为了防止窃听机器声音的间谍（侧信道攻击）获取蓝图，你不会直接发送蓝图。相反，你将蓝图拆分为两部分：秘密和一个随机掩码。你将它们混合在一起，让混合物通过一系列机器，并希望机器的噪音不会泄露原始秘密。

这篇论文旨在为这种混合过程建立数学保证，确保无论生产线有多长，该过程都有效。

问题：有“泄漏”的机器

在后量子密码学（为阻止未来量子计算机而需要的新数学）的世界里，工厂使用一种特定的机器，称为模约减（具体为"Barrett"和"Montgomery"约减）。

把这些机器想象成专用计算器。

旧观点：长期以来，我们只知道"Barrett"计算器会泄露一点点信息。我们并不了解"Montgomery"计算器的情况。
风险：如果一台机器泄露过多，间谍可以通过监听功耗，猜出随机掩码，并最终重构出秘密蓝图。

发现："1 比特屏障”

作者发现，Barrett 和 Montgomery 计算器都具有一种非常具体且安全的行为。他们称之为**"1 比特屏障”**。

类比：
想象你试图猜一个 1 到 1,000,000 之间的数字。

如果一台机器是糟糕的，它可能会将你的猜测范围缩小到仅 100 个数字。这是一个巨大的泄露。
如果一台机器是完美的，它根本不会给你任何提示；你仍然必须猜测那一百万个数字。
1 比特屏障意味着机器将你的猜测范围缩小到最多 2 个数字。

用论文的语言来说，这被称为PF-PINI(2)。这意味着对于机器产生的任何输出，只有两种秘密和随机掩码的组合可能产生该结果。就像机器在说：“我产生了这个结果，它只能来自秘密 A 或秘密 B。”由于存在数百万种可能性，将其缩小到仅两种是极其安全的。

这篇论文的贡献：

Montgomery 是安全的：他们证明了 Montgomery 计算器（用于许多新标准）与 Barrett 计算器一样，也具有这种"1 比特屏障”。
连锁反应：他们证明了如果你将这些计算器串联成一条长线（流水线），安全性并不会仅仅因为线路变长而变差。

解决方案：“新鲜掩码”刷新站

这篇论文为构建这些生产线引入了一条关键规则：必须在每台机器之间插入一个“新鲜掩码”。

类比：
想象一场接力赛，选手传递接力棒。

糟糕的比赛：如果选手 A 将接力棒传给选手 B，选手 B 再传给选手 C，接力棒会变得脏污和磨损。观察整场比赛的间谍可以拼凑出所有三名选手的线索，从而猜出终点。
解决方案（新鲜掩码）：在选手 A 和选手 B 之间，你暂停比赛。你拿起接力棒，用一条全新的、干净的毯子（新鲜掩码）将其包裹，然后交给选手 B。接着，在 B 和 C 之间，你用另一条全新的毯子将其包裹。

因为毯子每次都是全新且随机的，监听选手 B 的间谍完全不知道选手 A 在做什么。比赛第一部分的“噪音”被彻底抹去了。

这篇论文从数学上证明，只要使用这些“新鲜掩码”刷新站，整个生产线的安全性仅取决于最后一台机器。前 99 台机器的安全性不那么重要，因为新鲜掩码会冲刷掉它们的泄露。

主要结果：“端到端”保证

作者使用了一个强大的计算机证明助手（称为Lean 4）来检查他们的数学推导。他们不仅仅是将其写下来，而是让计算机验证了每一个步骤，确保没有逻辑漏洞。

他们的结论：
如果你将一台台计算器（Barrett 或 Montgomery）串联成流水线，并在每一步之间放置一个“新鲜掩码”：

最终输出是安全的。
间谍能窃取的信息量被限制在"1 比特屏障”内（将猜测范围从数百万种可能性缩小到 2 种）。
无论你的流水线有 2 步还是 100 步，这种安全性都成立。流水线的长度不会使其变弱。

"Adams Bridge"案例研究

论文提到了一个名为Adams Bridge的真实硬件项目。

问题：先前的研究人员发现，Adams Bridge 硬件在某些步骤中忘记使用“新鲜掩码”，或者使用了并非完全安全的机器。
论文的裁决：作者并没有说"Adams Bridge 坏了”。相反，他们说："Adams Bridge 未能通过我们刚刚证明的特定测试。”
解决方案：他们表明，如果 Adams Bridge 添加缺失的“新鲜掩码”站，并确保每台机器都是安全类型，它将能通过测试。

一句话总结

这篇论文证明，如果你将安全的数学计算器串联起来，并在每一个计算器之间放置一个“新鲜随机盾牌”，无论链条有多长，整个系统都能抵御间谍攻击，且这一结论适用于未来抗量子安全中使用的两种主要计算器类型。

技术摘要：1 比特障碍的普适性

问题陈述
数论变换（NTT）是 NIST 后量子密码（PQC）标准 ML-DSA（FIPS 204）和 ML-KEM（FIPS 203）的计算骨干。这些标准的硬件实现依赖算术掩码来抵御侧信道攻击，特别是差分功耗分析（DPA）。虽然 $GF(2^n)$ 上的布尔掩码已建立组合性框架（例如 PINI），但素数 $q$ 上 $\mathbb{Z}_q$ 的算术掩码却面临独特挑战。

QANARY 计划（论文 1–6）的先前工作建立了结构依赖性分析并量化了特定组件的安全裕度，特别是证明了 Barrett 约减满足"1 比特障碍”（PF-PINI(2)）。然而，仍存在两个关键缺口：

任意流水线深度：先前的组合定理仅限于两阶段。对于具有新鲜阶段间掩码的任意 $k$ 阶段流水线，缺乏形式化保证。
Montgomery 约减：虽然 Barrett 约减已得到表征，但 Montgomery 约减（NTT 硬件中使用的第二种标准模约减，在 ML-DSA 和部分 ML-KEM 实现中占主导地位）缺乏正式的 PF-PINI 表征。
统一端到端界限：不存在单一的、机器检查的基数界限，能够将由蝴蝶运算、Barrett 约减和 Montgomery 约减组成的任意流水线的结果整合起来。

方法论
本文采用 Lean 4 证明助手进行形式化验证。该方法严格具有构造性，零 sorry（未证明的假设）且零非标准公理。方法论依赖于：

PF-PINI 定义：使用素域探针隔离非干扰（PF-PINI）参数，该参数量化了单算术掩码下单根导线小工具的泄露量。若任何输出值的原像基数至多为 $M$ ，则小工具为 PF-PINI( $M$ )。
流水线建模：定义一个 $k$ 阶段流水线，其中每个阶段 $G_i$ 是一个 PF-PINI 小工具，由新鲜随机掩码分隔。流水线输出通过递归方式计算。
组合分析：证明新鲜阶段间掩码“擦除”了中间阶段的泄露参数，使得最终界限仅取决于最后阶段的参数。
硬件忠实建模：对 Montgomery 约减进行建模，以考虑硬件寄存器宽度和回绕行为，特别是分析碰撞偏移量 $2^{w-s}$ 。

主要贡献
本文做出了四项主要贡献，均在 Lean 4 中形式化：

$k$ 阶段组合定理（定理 3.1）：
该定理将先前的两阶段组合结果推广至任意深度 $k \ge 1$ 。它证明了对于具有新鲜阶段间掩码的小工具流水线 $G_0, \dots, G_{k-1}$ ，输出原像的基数受限于：
$| \{ (m, f) : \text{流水线输出} = v \} | \le G_{k-1}.\text{maxMult} \cdot q^{2k-2}$
关键在于，该界限是由最后阶段决定的；所有中间阶段的参数均被新鲜掩码擦除。
Montgomery 约减是 PF-PINI(2)（定理 4.3）：
本文形式化证明了 Montgomery 约减满足 PF-PINI(2) 属性，其结构与 Barrett 约减镜像对应。它表明硬件忠实的 Montgomery 映射具有“双分支”结构（取决于是否发生回绕），导致原像基数至多为 2。定理 4.7 进一步确立了该界限的紧性，表明对于标准参数（ML-KEM 和 ML-DSA），重数恰好为 2。
端到端重数界限（定理 5.1）：
通过将 $k$ 阶段组合定理与 Barrett（论文 5）、Montgomery（本文）和蝴蝶运算（论文 4）的具体 PF-PINI(2) 结果相结合，本文建立了一个统一界限。对于任何 $k$ 阶段流水线，若每个阶段满足 $\text{maxMult} \le 2$ ，则输出原像基数受限于：
$2 \cdot q^{2k-2}$
在具有均匀掩码的一阶探测模型下，这对应于每次观测的条件概率界限 $2/q$ ，且独立于流水线深度 $k$ 。
实证发现的形式化锚定（定理 5.4）：
本文提供了一个经 Lean 验证的条件：如果流水线中任何阶段具有 $\text{maxMult} \ge 3$ （例如未掩码阶段），则端到端界限的假设失效。这形式化地锚定了先前对"Adams Bridge"PQC 加速器（论文 1、2 及外部工作）的实证和结构分析，确认该设计中特定的未掩码配置不符合深度独立界限的充分条件。

结果

1 比特障碍的普适性：本文确认"1 比特障碍”（原像基数为 2）适用于 NIST PQC 硬件中使用的两种标准模约减（Barrett 和 Montgomery）。
深度独立性：形式化证明表明，只要使用新鲜阶段间掩码且每个阶段满足 PF-PINI( $\le 2$ )，向流水线添加阶段不会降低每次观测的泄露界限。
验证状态：整个工件包含三个定理模块中的 20 个声明，在 1,753 个作业中构建完成，零错误、零 sorry，且无原生决策过程。

意义与主张
本文将自己定位为掩码 NTT 硬件形式化验证计划的完成。其意义在于为硬件设计人员提供了一个定量的、机器检查的组合基础。

对于认证：推导出的基数界限（ $2 \cdot q^{2k-2}$ ）提供了架构级别 DPA 抗性论证所需的特定证据，补充了 SILVER 和 maskVerif 等门级工具。
对于设计人员：它提供了一条规定性的修复路径：为了实现深度独立界限，设计人员必须确保每个阶段均为 PF-PINI( $\le 2$ )，并在阶段之间插入新鲜掩码。
主张的谦逊性：作者明确指出，概率和最小熵解释（例如 $2/q$ ）是基数界限的非形式化语义推论，并未在 Lean 中进行机械形式化。此外，关于 Adams Bridge 分析，本文仅声称特定配置未能满足定理 5.1 的充分条件；它并未声称硬件“已损坏”或“不安全”，承认替代框架或更强模型可能会得出不同结论。这项工作被框架化为一种组合分析工具，而非针对特定实现的确切安全裁决。