💻 computer science

Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators

本文提出了一种包含结构依赖分析、新鲜掩码优化及布尔与算术单认证距离检查（SADC）的四层验证体系，成功将侧信道掩码验证扩展至百万门级后量子密码加速器，在 Adams Bridge ML-DSA/ML-KEM 硬件上实现了秒级分析并生成了可交叉验证的数学证书，从而大幅缩减了人工审查范围并支持了生产级芯片的预硅片侧信道证据生成。

原作者： Ray Iskander, Khaled Kirah

发布于 2026-04-17

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Ray Iskander, Khaled Kirah

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

这篇论文介绍了一种名为 QANARY（量子金丝雀）的新工具，它的作用是像煤矿里的金丝雀一样，在量子计算机真正威胁到来之前，提前发现并预警那些“不安全”的加密芯片设计。

为了让你更容易理解，我们可以把这篇论文的核心内容想象成检查一座巨大的、正在建造中的“数字金库”。

1. 背景：为什么要检查？

现在的银行和通信系统都在升级，以防御未来的“量子计算机”黑客。这种新加密技术叫后量子密码学（PQC）。

问题：黑客不仅会偷看数据，还会通过测量芯片的耗电量（就像听金库锁芯转动的声音）来猜出密码。
对策：工程师们给密码加了一层“迷雾”（称为掩码）。这就好比把一把钥匙拆成两半，分别由两个不同的守卫拿着。只有当两半合在一起时，才能打开锁。只要黑客只能偷看其中一个守卫，他就永远猜不出钥匙是什么。
挑战：在芯片里，这种“拆钥匙”的操作非常复杂，涉及数百万个微小的逻辑门（就像金库里有几百万个齿轮）。人工检查这些齿轮是否真的把钥匙分开了，就像试图在几秒钟内数清大海里的沙子，根本不可能。现有的自动检查工具要么太慢，要么只能检查很小的部分。

2. 核心创新：QANARY 工具的四层过滤网

作者开发了一套四层检查系统，专门用来快速扫描这些巨大的芯片设计（117 万个逻辑单元），找出哪里可能“漏风”。

想象你在检查一列长长的火车（芯片），看看有没有乘客（秘密信息）混进了错误的车厢。

第一层：结构依赖分析（D0/D1）—— “看地图”
- 原理：不看具体的乘客，只看轨道。如果两条轨道（代表钥匙的两半）在某个地方汇合了，那就意味着它们可能重新拼在了一起，这是危险的。
- 效果：这一步非常快，几秒钟就能扫完整个芯片。但它很“笨”，只要看到轨道汇合就报警，哪怕实际上并没有乘客真的在那里相遇。所以它会报很多“假警报”。
第二层：多周期分析（MC-D1）—— “看时间轴”
- 原理：有些轨道汇合不是马上发生的，而是过了几个时钟周期（几秒后）才发生。就像乘客在第一节车厢分开，但在第十节车厢又碰头了。这一步专门检查这种“跨时间”的汇合。
- 效果：它发现了很多第一层没看到的隐患，把原本以为安全的 12 个模块重新标记为“有风险”。
第三层：新鲜掩码精修（FM）—— “检查新面具”
- 原理：有时候，虽然轨道汇合了，但中间突然加了一个全新的、随机的“面具”（随机数），把之前的秘密信息给擦掉了。
- 效果：这一步能排除掉一部分因为加了随机数而实际上安全的“假警报”。
第四层：算术 SADC（统计代数检查）—— “数学验尸”
- 原理：这是最厉害的一层。对于前面剩下的那些“疑似危险”的线路，它不再只看轨道，而是用超级强大的数学逻辑（SMT 求解器）去模拟：“如果黑客真的在这里偷看，他到底能不能算出钥匙？”
- 效果：
  - 它把原本 363 个“疑似危险”的线路，198 个确认为绝对安全（给了数学证书）。
  - 剩下165 个被标记为“需要设计师重点排查”。
  - 0 个被遗漏（没有漏网之鱼）。

3. 实际战果：在“亚当斯大桥”上的测试

作者把这套工具用在了一个真实的、巨大的开源加密芯片项目（Adams Bridge，包含 ML-KEM 和 ML-DSA 标准）上。

规模：这个芯片有117 万个逻辑单元，相当于一个小型城市的大小。
速度：
- 第一层扫描只用了8.7 秒。
- 整个四层深度检查（包括最难的数学验证）只用了3 分钟（在普通单核电脑上）。
对比：以前最厉害的精确检查工具（像 SILVER 或 Coco-Alma），只能检查几千个单元，遇到这么大的芯片就会“死机”或超时。而 QANARY 不仅跑完了，还给出了精确的数学证明。
结果：它把原本需要人工检查几百个“假警报”的工作量，压缩成了165 个真正需要关注的“嫌疑人”，并且为其中一半提供了“无罪证明”。

4. 为什么这很重要？

从“猜”到“证”：以前，面对这么大的芯片，工程师只能靠猜或者抽样检查。现在，他们可以在芯片造出来之前（Pre-Silicon），就拿到数学上确凿的证据，证明哪些地方是安全的。
节省成本：如果芯片造出来才发现有漏洞，重做芯片的成本是天文数字。QANARY 能在设计阶段就把问题揪出来。
双重验证：为了确保工具自己没算错，作者用了两个完全不同的数学引擎（Z3 和 CVC5）互相核对，结果100% 一致，证明了结论的可靠性。

总结

这篇论文就像是在说：

“我们造了一个超级快的‘安检门’（QANARY），它能在一分钟内扫描完整个巨大的‘数字金库’。虽然它一开始会误报很多‘可疑人员’（假警报），但它通过四层过滤，最终能精准地告诉设计师：‘这 198 个人绝对安全，那 165 个人请你们亲自审问’。这让我们在面对未来量子黑客时，能更有信心地建造安全的加密硬件。”

这项技术对于通过美国 FIPS 140-3 等安全认证至关重要，因为它提供了一种可扩展的、数学上可信的方法来证明硬件的安全性。

这是一份关于论文《Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators》（掩码 NTT 硬件的结构依赖分析：后量子密码加速器的可扩展预硅验证）的详细技术总结。

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

随着 ML-KEM (FIPS 203) 和 ML-DSA (FIPS 204) 的标准化，构建抗侧信道攻击的后量子密码（PQC）硬件加速器变得至关重要。掩码（Masking）是主要的防御手段，其核心安全不变量是：没有任何组合逻辑路径允许同一秘密的两个或多个份额（shares）汇聚，否则会在功耗中产生可观察的秘密函数。

然而，现有的验证工具面临以下挑战：

可扩展性差：精确的掩码验证工具（如 SILVER, Prover, Coco-Alma）通常仅适用于几千个门电路的小规模模块（如 S-box），无法扩展到百万级门电路的生产级 PQC 加速器。
算术掩码与流水线复杂性：PQC 基于数论变换（NTT），涉及大域上的算术掩码（模 $q$ 加法/乘法）和深流水线。现有的单周期分析工具无法捕捉跨寄存器的多周期依赖路径，导致漏报（False Negatives）。
验证瓶颈：手动审查无法扩展，而基于轨迹的差分功耗分析（DPA）需要流片后的硬件，且可能遗漏特定数据或罕见控制路径下的泄漏。

2. 方法论 (Methodology)

作者提出了名为 QANARY 的工具，采用四阶段验证层级，将结构依赖分析与分布性检查相结合，实现了从 RTL 到网表的预硅验证。

核心阶段：

D0/D1 结构依赖分析 (Structural Dependency Analysis)：
- 原理：基于探针模型（Probing Model），检查每个信号线的组合扇入是否同时依赖于秘密份额 $s_0$ 和 $s_1$ 。
- 标签格 (Label Lattice)：使用 $\{ \bot, S_0, S_1, BOTH \}$ 格，通过拓扑传播标记信号线。若某线标记为 $BOTH$，则结构上不安全。
- 多周期扩展 (MC-D1)：引入固定点迭代算法，将依赖标签跨越寄存器（DFF）边界传播。这能发现单周期分析无法看到的跨寄存器份额汇聚（Cross-register convergence）。
- 特点：这是必要但不充分的条件。结构上标记为不安全的线，可能因代数抵消（如新鲜随机数）而实际上是安全的（假阳性），但结构上安全的线一定是安全的（零假阴性）。
新鲜掩码细化 (Fresh Masking Refinement, FM)：
- 检查结构上不安全的线是否被新鲜随机数（Fresh Randomness）重新掩码（即随机数作为异或掩码，使输出均匀分布）。如果是，则提升为安全。
布尔 SADC (Boolean Single-Authentication Distance Checking)：
- 针对布尔掩码模块，通过重参数化（将份额 $s_0, s_1$ 替换为秘密 $x$ 和掩码 $m$ ），利用 SMT 求解器（Z3）验证输出分布是否独立于秘密。
算术 SADC (Arithmetic SADC)：
- 创新点：针对 PQC 中的算术掩码（模 $q$ ），提出了一种基于**值独立性（Value-Independence）**的检查方法。
- 重参数化：将算术份额关系 $s_0 = (x - s_1) \mod q$ 符号化，构建两个秘密 $X, X'$ 的副本，检查是否存在 $X \neq X'$ 导致输出不同的情况。
- 双求解器验证：使用 Z3 和 CVC5 独立求解，确保结果无偏差。

3. 主要贡献 (Key Contributions)

生产级规模的结构依赖验证：
- 将分析扩展到 117 万单元 的 Adams Bridge ML-DSA/ML-KEM 加速器（30 个掩码子模块）。
- 单周期分析（SC-D1）在 8.7 秒 内完成；多周期分析（MC-D1）在 231.8 秒 内完成。证明了结构验证是下游精确验证可扩展的前提。
多周期结构重分类 (MC-D1)：
- 通过 MC-D1，将 12 个在单周期分析中被标记为“安全（Clean）”的模块重新分类为“不安全（Flagged）”。
- 揭示了跨寄存器边界导致的份额汇聚，这是传统单周期工具完全遗漏的漏洞。
四阶段层级与算术 SADC：
- 在 5,543 单元的 ML-KEM Barrett 模约减模块上，该层级成功处理了 363 个结构标记的不安全线：
  - 198 条 (54.5%) 被机器验证为第一阶安全（基于算术值独立性）。
  - 165 条 被标记为候选不安全（作为设计师排查的可靠上界）。
  - 0 条 为不确定（Indeterminate）。
- 所有 363 个结果均通过 Z3 和 CVC5 交叉验证，零分歧。
可复现性与双重求解器验证：
- 提供了完整的复现工件（Docker, 脚本，证据 JSON）。
- 引入了 17 项强制性自检查，确保 SMT 编码的正确性。
- 首次将算术掩码的值独立性检查集成到 Yosys 驱动的结构验证流水线中。

4. 实验结果 (Results)

Adams Bridge 加速器分析：
- SC-D1：识别出 59,061 条不安全线。15 个模块安全，12 个不安全。
- MC-D1：识别出 614,126 条不安全线（增加了 10.4 倍）。其中 8,487 条是真正的“收敛点”（Root causes），其余为传播效应。
- 关键发现：ML-KEM Butterfly 模块在单周期分析中显示 0 条不安全线，但在多周期分析中暴露出 59,242 条不安全线，证实了跨寄存器依赖的严重性。
Barrett 模约减模块：
- 通过四阶段流水线，将原本需要人工审查的 363 条线，缩减为 165 条高优先级排查对象，并提供了 198 条机器验证的安全证书。
- 运行时间仅需约 3 分钟（单核）。
基准测试：
- 在 DOM AND 参考门电路上，流水线消除了 100% 的结构假阳性，与已知安全证明一致。
- 与 Coco-Alma 的对比显示，两者在定义上存在差异（SADC 基于稳定态单探针，Coco-Alma 包含瞬态/毛刺模型），但在可验证范围内结果一致。

5. 意义与影响 (Significance)

填补了验证空白：这是首个在生产级规模（百万级单元）的算术掩码 PQC 硬件上实现自动化门级验证的工具。现有的精确工具无法处理此类规模。
平衡了精度与规模：通过“结构筛查 + 分布性细化”的层级策略，既保证了零漏报（Soundness），又通过机器验证大幅减少了人工审查的工作量（从数百条降至 165 条可操作项）。
预硅验证能力：能够在流片前提供数学证明的安全证书和明确的漏洞上界，对于 FIPS 140-3 认证和 PQC 硬件设计迭代至关重要。
互补性：该工具不替代精确验证或物理测量，而是作为中间层，将巨大的设计空间缩小到可管理的范围，使后续的高成本验证（如模型计数或物理测试）变得可行。

总结：QANARY 工具通过创新的 MC-D1 多周期分析和算术 SADC 值独立性检查，成功解决了后量子密码硬件加速器中掩码验证的可扩展性难题，为大规模 PQC 硬件的安全设计提供了关键的预硅验证手段。