PQC-Assay

（原名 "Assay"）

使用 SAW → Cryptol → Isabelle pipeline，对后量子参考 C 代码及其规范进行机器检查。 PQC-Assay 运行与 Apple 在其 2026 年 `corecrypto` 工作中所使用的相同的 SAW → Cryptol → Isabelle pipeline，用于验证 ML-DSA (FIPS 204) 的 PQClean 参考 C 代码。它没有使用任何 Apple 的代码或理论；Isabelle 规范是根据 FIPS 204 编写的。 当前的范围是 `reduce.c` 算术层（两条路径）和正向 NTT（功能等效性 + 机器检查的无溢出 / 系数边界结果）。 Montgomery reduction 是 NTT 使用的一种实现手段；它未在 FIPS 204 中定义。这些都不是生产环境中发布的优化/汇编代码（参见[路线图](docs/ROADMAP.md)）。 ## 已证明的内容 `make verify` 检查两条路径（exit 0）： - **SAW (C ≡ Cryptol)** — 逐位验证： - `reduce.c` 层：`montgomery_reduce`（`−2³¹·Q ≤ a ≤ Q·2³¹`）、`reduce32`（`a ≤ 2³¹−2²²−1`）、`caddq`、`freeze` — 这些还断言在范围内没有有符号溢出 UB。 - 在二进制补码包装（`-fwrapv`）下的正向 NTT `ntt(a[256])`。这对于所有输入都是功能等效的；无溢出性在 Isabelle 中单独证明（见下文）。 变异测试确认 reduce 证明是非空洞的，并且 CI 将提取出的 Isabelle 模型与 SAW 检查的 Cryptol 模型进行了 diff 对比。 - **Isabelle (模型 ≡ 规范)** — 整个 `reduce.c` 层，没有 `sorry`/`oops`： - `montgomery_reduce` 满足 `is_montgomery_reduction`（`2³²·r ≡ a (mod Q)`，`−Q < r < Q`），范围在 `−2³¹·Q ≤ a < 2³¹·Q`。 - `caddq`（保持余数，将 `[−Q,Q)` 映射到 `[0,Q)`）；`reduce32`（保持余数，在前提 `a ≤ 2³¹−2²²−1` 下，输出在真实窗口 `[−6283009, 6283008]` 内）；`freeze = caddq∘reduce32`（输出在 `[0,Q)` 内），已进行组合证明。 - **Isabelle (正向 NTT 无溢出)** — `ntt_overflow_free`，没有 `sorry`/`oops`：对于每个系数都在 `±(2³¹−2²⁷)` 内的输入，模型 NTT 在所有 8 个层级中保持每个系数 `< 2³¹`，因此**没有 `int32` 加/减法溢出**，并且每个 `montgomery_reduce` 输入都保持在范围内。 这是 `-fwrapv` 证明所回避的系数边界组合——证明是通过对 8 个层级进行归纳完成的（每个层级迭代一个引理，montgomery 输出边界 `|t| < Q`），而不是通过 SAW 展开。C 端的声明（参考 NTT 没有有符号溢出 UB）是通过将其与 `-fwrapv` 的 C≡模型等效性组合得出的；最后这一步是经过论证的元步骤，并未单独进行机器化验证（参见 [`docs/ASSUMPTIONS.md`](docs/ASSUMPTIONS.md)，路线图 v1.5）。 与 SAW 路径链接后，这使得完整的 `reduce.c` 算术层实现了 C ≡ 规范（每个函数都在其证明的输出窗口内计算出正确的模 Q 余数），此外还得到了正向 NTT 的机器检查系数边界 / 无溢出结果。 在此过程中，我们在 PQClean 的 reduce.c 文档注释中发现了两个 off-by-one 错误 —— `montgomery_reduce`（严格边界在一个不可达的端点处失败；OF-1）和 `reduce32`（文档记录的下界 `−6283008` 在其自身的单侧前提下可达为 `−6283009`；OF-2）。两者都是文档/契约问题，而不是计算错误。参见 `docs/ASSUMPTIONS.md`。 ## 范围与限制 两名外部审阅者（形式化方法；应用 PQC）阅读了此文。他们的总结是：证明是正确的，范围界定也很客观，但它针对的是较简单的函数。 - `montgomery_reduce` 是整个栈中最不容易出 bug 的部分 —— 无分支，只有两次乘法和一次位移，在 pq-crystals 中多年未变。ML-DSA 真正的正确性风险在于跨 NTT/InvNTT 的 reduction 边界组合（例如 ePrint [2026/1032](https://eprint.iacr.org/2026/1032)，一个通过了测试向量的优化路径溢出；以及 Apple 的 SAW 工作在 ML-DSA InvNTT 中发现的缺失 reduction 错误）。单原语证明无法触及这一点。带有系数边界跟踪的正向 NTT 是下一步计划。 - 已验证的范围（`|a| ≤ 2³¹·Q ≈ 2⁵⁴`）比 ML-DSA 提供给该函数的任何输入都要宽约 256 倍（调用点产生的值 `≲ Q² ≈ 2⁴⁶`），这就是为什么 OF-1 的端点在实践中从未出现的原因。 - `montgomery_reduce` 在 ML-DSA-44/65/87 中是相同的，因此 "-44" 的限定只是表面上的，该结果适用于所有三个。 - 这是参考 C 代码。实际发布的代码（AVX2/aarch64；OpenSSL、BoringSSL、AWS-LC；PQ Code Package `mldsa-native`）是不同的，并使用其他工具（CBMC、HOL-Light）进行了验证。将此 pipeline 指向 `mldsa-native` 是 v2 的计划。 因此：这是一个在第三方参考 C 代码上运行的端到端 pipeline，外加两个次要的上游文档修复（OF-1，OF-2）。它不是一个 ML-DSA 的保障结果。 ## 背景（如果您对形式化验证还不熟悉） 2026 年 5 月，Apple 开源了 [`corecrypto` 的形式化验证](https://github.com/apple/corecrypto/tree/2026-05)，这是 Apple 设备上的加密技术，涵盖 ML-KEM 和 ML-DSA (FIPS 203/204)。这里的形式化验证是指通过机器检查来证明代码对于所有输入都能计算出规范所定义的结果，而不仅仅是测试碰巧命中的那些情况。Apple 使用了 [Galois](https://github.com/GaloisInc/saw-script) 的 SAW + Cryptol 和 [Isabelle](https://isabelle.in.tum.de/) 证明器，并捕获了测试遗漏的 bug。PQC-Assay 将相同的公开方法应用于第三方参考 C 代码。 ## Pipeline ``` target C subroutine │ (1) hand-translate ▼ Cryptol model ──(2) SAW: C ≡ Cryptol──► ✔ │ (3) cryptol-to-isabelle ▼ Isabelle model ──(4) model ≡ FIPS spec──► ✔ (reduce.c layer) ▲ spec written from FIPS 204; no Apple artifacts ``` 详见 [`docs/PIPELINE.md`](docs/PIPELINE.md)。 ## 复现 在 Apple Silicon 上的 macOS（锁定工具链；参见 `docs/ASSUMPTIONS.md`）。 ``` ./scripts/setup.sh # install pinned SAW, Cryptol, Isabelle, cryptol-to-isabelle ./scripts/setup_isabelle_cryptol.sh # AFP + build the SAW 'Cryptol' Isabelle session (slow, once) make verify # both legs; non-zero exit = a proof failed make saw # SAW leg only (fast, no Isabelle) ``` ## 布局 | 路径 | 内容 | |------|------| | `target/` | 正在验证的 C 代码，带有锁定的出处 | | `model/` | 原语的 Cryptol 模型 | | `proof/` | SAW 脚本 (C ≡ Cryptol) | | `spec/` | Isabelle 规范 + 等效性证明 | | `docs/` | 路线图、假设、pipeline、报告 | | `scripts/` | 工具链设置和 pipeline 编排 | ## 工具 来自 Galois 的 SAW + Cryptol 和 `cryptol-to-isabelle` (saw-script 1.5.1)；Isabelle + AFP。Pipeline 结构遵循 Apple 发布的 corecrypto 方法；未使用任何 Apple 的代码或理论。 ## 许可证 项目代码：[MIT](LICENSE)。`target/` 中引入的 C 代码是 PQClean/pq-crystals 参考代码（CC0；参见 [`target/README.md`](target/README.md)）。Isabelle 规范是原创的；不包含任何 Apple 的成果。

标签：代码等效性验证, 后量子密码学, 定理证明, 密码学实现, 形式化验证, 通知系统