Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware

以下是论文《机器验证的掩码 Barrett 约简基数界限：后量子密码硬件中的 1 比特侧信道泄漏屏障》的详细技术总结。

1. 问题陈述

后量子密码（PQC）标准，如 ML-KEM（FIPS 203）和 ML-DSA（FIPS 204），高度依赖数论变换（NTT）流水线。这些流水线由线性的“蝴蝶”阶段和非线性的模约简阶段组成，通常使用Barrett 约简实现。

尽管现有的形式化验证框架（ISW、t-SNI、PINI、DOM）为 $GF(2)$上的布尔掩码提供了强有力的保证，但它们缺乏针对**素域（$\mathbb{Z}_q$）上算术掩码**（特别是 Barrett 约简）的机器验证特征描述。

• 差距所在：硬件实现（例如"Adams Bridge"设计）往往存在侧信道漏洞，因为 Barrett 约简中的非线性条件减法破坏了标准组合定理所假设的仿射结构。
• 核心问题：在一阶算术掩码下，Barrett 约简电路内部导线的精确泄漏界限是多少？之前的工具无法提供通用的、机器验证的答案，导致 FIPS 140-3 认证存在不确定性。

2. 方法论

作者采用基于 Lean 4 证明助手和 Mathlib 库的形式化验证方法。

• 形式化：他们在 $\mathbb{Z}_q$（其中 $q$ 为模数）上代数地定义了 Barrett 内部导线映射。映射 $f_x(m)$ 接收一个秘密值 $x$ 和一个随机掩码 $m$，基于由条件减法决定的双分支结构产生输出。
• 证明策略：他们不是模拟特定实例，而是证明适用于所有 $q > 0$ 和移位参数 $s$ 的通用定理。
• 关键概念：他们分析原像基数：对于固定的秘密值 $x$ 和特定的输出值 $v$，有多少个不同的掩码 $m$ 可能产生 $v$？
• 工具链：该工件包含 12 个已证明的结果，且零 sorry（无未完成的证明），确保每一步都由 Lean 内核验证。

3. 主要贡献

A. 三分定理

论文证明了 Barrett 内部导线映射表现出三值原像结构。对于任何秘密值 $x$ 和任何输出值 $v$，使得 $f_x(m) = v$ 的掩码 $m$ 的数量恰好为 0、1 或 2。

• 机制：条件减法创建了两个仿射分支（$\mathbb{Z}_q$ 中的平移）。任何值的原像最多包含两个候选值的子集：$\{x - v, x - v + r\}$，其中 $r = 2^s \mod q$。
• 通用性：这对任何模数 $q$ 和移位 $s$ 均成立，独立于特定的 PQC 参数。

B. 1 比特屏障

基于三分定理，作者建立了一个通用的泄漏界限：

• 最大多重性：由于产生单个输出的掩码最大数量为 2，观察到特定输出值的最大概率为 $2/q$。
• 最小熵界限：条件最小熵 $H_\infty(\text{output} \mid x)$ 的下界为 $\log_2(q) - 1$。
• 解释：在一阶探测下，Barrett 约简每条内部导线最多泄漏 1 比特 的最小熵。这是一个“保守”界限，因为许多输出值是不可达的（原像计数 = 0），意味着实际泄漏通常严格小于 1 比特。

C. PF-PINI 框架

作者引入了素域 PINI（PF-PINI），这是一种针对 $\mathbb{Z}_q$ 上算术组件的新安全度量：

• 定义：如果原像基数有界于 $k$，则一个组件为 PF-PINI($k$)。
• 实例化：
  • 蝴蝶阶段：满足 PF-PINI(1)（完美双射，除掩码外零泄漏）。
  • Barrett 约简：满足 PF-PINI(2)（即 1 比特屏障）。
• 组合观察：他们观察到（尽管尚未形式化证明），如果流水线阶段之间通过新鲜级间掩码分隔，则组合流水线的最大多重性为 $\max(k_1, k_2)$。这意味着 1 比特屏障会传播至整个 NTT 流水线。

4. 结果与分析

• 机器验证证明：该工件包含 12 个已验证定理，包括三分定理、紧性证明（表明计数=2 是可达的）以及 PF-PINI 实例化。
• 支持差距发现：分析揭示了“不可达”的输出值（原像计数 = 0）。这是一个安全特性而非缺陷，因为它减少了攻击者的有效信息。
• Adams Bridge 案例研究：论文分析了"Adams Bridge"硬件实现：
  • 级内失效：先前的工作（论文 1 和 2）表明，由于缺乏中间掩码的份额交互导致了漏洞。
  • 级间失效：本文指出 Adams Bridge 未能应用级间新鲜掩码。因此，PF-PINI 组合界限不适用，导致泄漏相乘（$k_1 \times k_2$）而非保持为最大值（$\max(k_1, k_2)$）。这解释了为何尽管单个 Barrett 门存在 1 比特屏障，该设计仍然脆弱。
• 定量影响：
  • 对于 ML-KEM（$q=3329$）：泄漏 $\le 1$ 比特（最小熵 $\ge 10.70$ 比特）。
  • 对于 ML-DSA（$q=8,380,417$）：泄漏 $\le 1$ 比特（最小熵 $\ge 21.99$ 比特）。

5. 意义

• 认证就绪性：1 比特屏障为硬件设计师提供了通用的、机器验证的证书。它允许评估人员在不重新验证特定参数集的情况下，认证基于 Barrett 的实现以符合 FIPS 140-3 标准。
• 设计指导：它阐明了安全性的主要架构要求是新鲜级间掩码。如果实现了这一点，Barrett 约简的非线性性质不会使 NTT 流水线的安全性受到超过可忽略的 1 比特损失的影响。
• 方法论转变：该论文将侧信道分析从经验模拟和基于 SAT 的检查转变为内核验证的代数证明，为 PQC 硬件验证设立了新标准。
• 完成五篇论文计划：这项工作填补了系列论文中留下的空白，从工具构建（论文 1）和攻击量化（论文 2）推进到代数基础（论文 3）、线性组合（论文 4），最后是非线性特征描述（论文 5）。

6. 局限性与未来工作

• 组合证明：关于具有新鲜掩码的组合流水线满足 $\max(k_1, k_2)$ 的断言目前是一个观察结果，而非形式化定理。
• 高阶掩码：结果仅限于一阶掩码（$t=1$）。高阶安全性需要分析多条导线上的联合原像。
• 熵形式化：虽然代数界限已得到证明，但信息论最小熵界限依赖于尚未完全上游化到 Mathlib 的标准定义。
• 其他约简：结果特定于 Barrett 约简；Montgomery 约简和竖式约简需要单独分析。

总之，本文确立了Barrett 约简在一阶算术掩码下本质上是安全的，只要流水线阶段之间应用了新鲜掩码，每条导线泄漏的信息不超过 1 比特。这为保护下一代 PQC 硬件提供了严谨的数学基础。