SPARK 中的基础密码学

# 使用 AI 进行形式化软件验证：前沿 AI 生成了 SPARK... 来源：https://www.adacore.com/blog/foundational-cryptography-in-spark 最近，Anthropic (https://www.anthropic.com/) 发布了一篇研究文章，宣扬了 LLM 在形式化软件验证中的应用 (https://www.adacore.com/blog/foundational-cryptography-in-spark)。我们很高兴他们对此感到兴奋！当然，我们一直在谈论这件事——今年如此，之前也是如此。我们同意 AI 使得形式化软件验证达到了前所未有的可行性。以下是我们的最新示例。 七月，美国国家安全局 (https://www.nsa.gov/) 向 GitHub (https://github.com/NationalSecurityAgency) 发布了一个密码算法形式化规范的仓库。他们将该仓库命名为 Foundation (https://github.com/NationalSecurityAgency/Foundation)。作为其工作成果的演示，他们包含了一个经过证明的 Rust 实现的 AES。自然，我们将此视为展示 SPARK 的机会，更重要的是，展示 SPARK + AI 的机会。 您可以在我们的 fork 中找到我们的工作成果：[此处](https://github.com/manthonyaiello/Foundation/tree/spark-v1.0)；`spark` 文件夹中的 README 请见[此处](https://github.com/manthonyaiello/Foundation/tree/spark-v1.0/spark)。 借助 AI，我们在 SPARK 中获得了 AES（128、192、256）、SHA-256 和 HMAC-SHA-256 的形式化规范及已证明的实现。无需直接的人工干预，尽管我们审查了规范并提出了一些小的风格（非功能性）改进建议。这是 SPARK Platinum 代码：完全的功能正确性。我们对工作的正确性有信心，因为我们从四个不同角度验证了正确性： 1. SPARK 规范被证明在选定的消息、密钥和文本长度上与 NSA 的 Cryptol (https://tools.galois.com/cryptol) 规范功能等价； 2. SPARK 实现被证明满足其功能规范； 3. SPARK 实现在选定的消息、密钥和文本长度上被证明与 NSA 的 Cryptol 规范功能等价；以及 4. SPARK 已针对 Cryptol 规范进行了测试 因此，尽管 SPARK 规范和实现完全由 AI 编写，但我们拥有多项形式化证明，以及达到 100% MC/DC 覆盖率的广泛基于规范的测试，证明 AI 的工作是正确且完整的。 ## NSA 的 Foundation Foundation 是 NSA 的一个公开仓库，其中的密码算法使用 Galois (https://www.galois.com/) 的 Cryptol 进行形式化规范。Cryptol 是一种专门为密码学规范设计的形式化规范语言。NSA 提供了许多算法；对于其中一些算法，还提供了 Rust 参考实现。 ## 我们的选择：AES、SHA-256、HMAC-SHA-256 作为起点，我们选择了三种算法： - AES (https://en.wikipedia.org/wiki/Advanced_Encryption_Standard)，涵盖所有三种密钥长度：128、199 和 256 位； - SHA-256 (https://en.wikipedia.org/wiki/SHA-2)；以及 - HMAC (https://en.wikipedia.org/wiki/HMAC)，使用 SHA-256 实例化 这些算法的细节超出了本篇博文的范围；上述链接指向它们的 Wikipedia 条目。 我们选择 AES 是因为它被广泛使用，因为 NSA 提供了 Rust 参考实现，而且它在规范编写上具有挑战性。 我们选择 SHA-256 是因为它同样被广泛使用，而且拥有第二种算法可以证明我们的方法是可复制的（即 AES 并非对 SPARK 来说特别容易处理）。 我们选择 HMAC 是因为三是一个不错的数字，而且它建立在 SHA-256 的工作之上。 此外，这三种算法展示了不同的关注特性： - AES 依赖于伽罗瓦域 GF(2) 和 GF(2⁸) 上的算术运算； - SHA-256 依赖于模字算术和可变长度消息的填充；以及 - HMAC 依赖于与流处理的组合。 ## 我们的工作 对于每种算法，我们都遵循相同的流程。以下示例将聚焦于 AES。 ### SPARK 规范 我们根据 Cryptol 编写了 SPARK 规范。每个 SPARK 规范的编写都尽量减小与 Cryptol 之间的语法和语义距离：这使得将两个规范并排阅读并验证 SPARK 的正确性变得更加容易。 有时这非常自然。例如，Cryptol 中： ``` xTimes : [8] -> [8] xTimes b = b << 1 ^ (if head b then 0x1b else 0x00) ``` 对应的 SPARK： ``` function xTimes (B : Byte) return Byte is (Interfaces.Shift_Left (B, 1) xor (if Head (B) then 16#1b# else 16#00#)); ``` 但 Cryptol 是为密码学规范设计的；SPARK 是一种通用语言。因此，在许多地方我们需要在 SPARK 中说得更多或以不同的方式表达： ``` foreign Cipher : {k} (Key k) => [Nr k + 1]Block -> Block -> Block Cipher ([w0] # ws # [wr]) in = state_final where state_initial = AddRoundKey in w0 state_rounds = foldl Round state_initial ws state_final = AddRoundKey (ShiftRows (SubBytes state_rounds)) wr ``` 对应的 SPARK： ``` function Cipher (W : Round_Keys; Input : Block) return Block is (AddRoundKey (ShiftRows (SubBytes (Foldl_Round (AddRoundKey (Input, W (0)), W (1 .. Nr - 1)))), W (Nr))); ``` Cryptol 拥有诸如 `foldl`、`split/join` 和 `pmult`/`pmod`（GF(2) 多项式上的运算）等原语；在 SPARK 中，我们通过预定义库引入这些操作。 仓库包含规范的详细讲解，将 Cryptol 和 SPARK 并排展示并讨论它们之间的差异。您可以在[此处](https://github.com/manthonyaiello/Foundation/tree/spark-v1.0/spark/doc/walkthroughs)找到它们。请注意，SPARK 规范是可执行的（大多数 SPARK 规范都是如此）；它被标记为 `Ghost`，以便在编译时可以将其移除。 最终，我们不必通过审查来验证 SPARK 规范的正确性；正如下面将展示的，我们证明了 SPARK 规范与 Cryptol 之间的功能等价性。 正确的规范完全自动获得，无需人工指导。原始规范完全可读，并且在减小与 Cryptol 规范之间的语法和语义距离方面做得非常出色。然而，我们确实仔细审查了 AES 规范，并提供了一些反馈和改进建议，进一步减小了语法距离。虽然这些改进有所帮助，但并非严格必要。 ### SPARK 实现 SPARK 实现通过声明操作上的后置条件为规范中对应的函数来与 SPARK 规范关联： ``` procedure Encrypt_Block (K : Key_Size; W : Round_Keys; State : in out Block) with Pre => Is_Round_Keys (K, W), Post => State = Spec.Dispatch.Cipher (K, W, State'Old); ``` 实现是命令式的。它们包含循环、就地状态操作，并为 SHA-256 和 HMAC 提供流处理功能。 实现完全自动获得，无需人工指导。前沿 AI 完全独立地编写了实现。 ### SPARK 证明 从概念上讲，SPARK 证明包含三个部分： 1. 运行时错误不存在性证明（SPARK Silver）。我们证明了规范（如果被执行）和实现（当被执行时）都不会遇到运行时错误。这在后面变得很重要：我们的另一个证明依赖于此。它还允许我们关闭所有运行时检查，从而提升性能。 2. 实现满足规范的证明（本例中为 SPARK Platinum）。由于 Cryptol 规范，进而 SPARK 规范，完整捕获了我们实现的功能需求，我们证明了实现的完全功能正确性。 3. 规范假定性质的证明（规范验证）。遵循 Cryptol，我们证明了例如 AES SBox 的表表示符合 SBox 的功能定义[1]。 总共，证明包含 71 个 SPARK 单元上的 4,085 项检查，外加按需运行的耗时 `SBox_Entries` 证明的 2,565 项检查。未使用任何逃逸机制：任何地方都没有 SPARK_Mode => Off，没有假设，没有理由说明。证明负担情况如下：23 个循环不变式；83 条断言；87 次引理调用。 此证明完全自动获得，无需人工指导。前沿 AI 独立完成了证明。 ### 通过 Cryptol 的 FFI 进行测试 Cryptol 提供了使用 C 调用约定的外部函数接口；SPARK 导出了其规范和实现函数的 C 接口。因此我们可以声明 SPARK 函数等于其 Cryptol 对应函数，如下所示： ``` prop_xTimes : [8] -> Bit property prop_xTimes b = spark_xTimes b == xTimes b prop_Dot : [8] -> [8] -> Bit property prop_Dot b c = spark_Dot b c == b • c ``` 这些性质列在一个文件中，并在 CI 中作为测试执行，使用 Cryptol 的 `check` 或 `exhaust` 命令。Cryptol 必须加载 SPARK 库且不得加载其他库（这样我们就不会，例如，意外地将 SPARK 与 Rust 进行测试），且在测试期间不得报告任何错误。Cryptol 必须报告通过的测试数量，对于穷举测试，必须报告 Q.E.D。 虽然这种测试很强，但仍然不够： 1. 在测试的 141 个性质中，只有 36 个性质的域足够小，可以用 `exhaust` 进行测试。 2. `check` 会抽取随机输入。如果我们固定种子，可以实现可重复测试，但我们选择不这样做，因为测试不是我们的主要验证手段。 3. `check` 的规模相对较小：1. 每种 AES 密钥大小的块和密钥扩展性质运行 1,000 次；整个密码运算性质各运行 5 次，因为 Cryptol 很慢。2. 对于 SHA-256 和 HMAC，每次随机测试在一组固定长度上检查一个随机输入。例如，`prop_Stream_Hash` 在从 0 到 128 字节的 11 个边界长度上运行 100 次测试，产生 1,100 个哈希值。`_long` 性质在从 562 到 3,837 字节的 10 个长度上运行 3 次测试（Cryptol 的参考哈希在长消息上很慢）。因此，虽然内容是随机的，但长度不是；没有任何测试超过 3,837 字节。 我们的变异测试提供了最强的证据，表明我们的测试是不够的。在我们注入到实现中的 84 个单行故障中，基于 FFI 的测试只发现了其中 68 个。通过测试的 16 个故障中，有 6 个是 `SHA256_Stream` 中的真实缺陷。SPARK 拒绝了所有这些故障，虽然是通过超时而非找到具体反例来实现的。 值得注意的是，我们通过 Cryptol 的 FFI 测试实现时确实获得了 100% MC/DC 覆盖率。由于从规范驱动（因此是基于需求的）测试中获得了这一覆盖率，我们有合理的信心认为实现中不存在非预期的功能[2]。 这些测试完全自动获得，无需人工指导。前沿 AI 独立完成了测试。 ### 与 SAW 的等价性证明 软件分析工作台（SAW (https://tools.galois.com/saw)）是 Galois 提供的一个工具，用于证明算法的两种形式化表示之间的功能等价性。SAW 能够原生处理 Cryptol，并提供了从低级表示导入软件实现的工具：对于 Rust，这是 MIR；对于其他语言，这是 LLVM。在 Foundation 仓库中，NSA 使用 SAW 证明了其 AES Rust 参考实现与其 AES Cryptol 规范的功能等价性。 我们使用 SAW 与 `gnat-llvm`（我们为 GNAT 编译器提供的 LLVM 后端），来证明我们的 SPARK 实现与 Cryptol 规范功能等价，同时也单独证明了我们的 SPARK 规范与 Cryptol 规范功能等价。这有点过度，但我们希望展示各种工具的能力，并为 AI 生成的规范和实现的正确性提供我们所能提供的最强保证。 我们使用 SAW 的 `llvm_verify` 来证明实现，断言每个实现入口点（例如 `Encrypt_Block`）与其 Cryptol 规范功能等价。我们通过使用 `pragma Assertion_Policy (Ghost => Check)` 启用 Ghost 代码执行来证明规范，这允许我们类似地使用 `llvm_verify` 来处理规范。为确保 SAW 证明不是空洞的，我们有意破坏实现并确认 SAW 报告反例。 SAW 中的 AES 规范和实现证明覆盖了每种密钥大小的所有输入。SAW 中的 SHA-256 规范和实现证明覆盖了 12 种选定的消息大小。SAW 中的 HMAC 规范和实现证明覆盖了 7 组选定的（密钥长度，文本长度）配对[3]。 这些证明完全自动获得，无需人工指导。前沿 AI 独立完成了这些证明。 ### 视觉总结 以下是各个部分如何配合以及我们建立的正确性证据的总结。 https://www.adacore.com/uploads/foundation-spark-relationships.svg ## 性能 ### 实现性能 在 Apple M1 Pro 上使用 GNAT FSF 16.1 和 rustc 1.95 以 `-O3` 编译测试，我们得到以下结果；所有时间单位为纳秒。 | 操作 | SPARK，关闭检查 | SPARK，开启检查 | Rust | 比率，关闭检查 | 比率，开启检查 | |---|---|---|---|---|---| | AES-128 Expand_Key | 131.9 | 130.0 | 403.7 | 0.33 | 0.32 | | AES-128 encrypt | 327.6 | 368.6 | 403.4 | 0.81 | 0.91 | | AES-128 decrypt | 775.0 | 778.1 | 722.2 | 1.07 | 1.08 | | AES-256 Expand_Key | 176.3 | 165.8 | 543.8 | 0.32 | 0.30 | | AES-256 encrypt | 468.3 | 520.2 | 569.0 | 0.82 | 0.91 | | AES-256 decrypt | 1111.8 | 1112.2 | 1034.3 | 1.07 | 1.08 | 总体而言，SPARK 实现比 Rust 实现更快。值得注意的是，这种加速并非来自禁用 SPARK 的运行时检查[4]。 然而，Rust 在解密上以极微弱优势胜出。原因是编译器未能内联对 `Inv_Mix_Byte` 的调用，导致该工作在 SPARK 中需要重复执行，而在 Rust 中是共享的。我们可以通过要求编译器使用 `pragma Inline_Always (Inv_Mix_Byte)` 来内联该函数来解决这个问题。经过这一改动，AES-128 解密降至 420 纳秒，AES-256 解密降至 600 纳秒；两者都显著优于 Rust[5]。 这个结果并不令人惊讶；我们知道 SPARK 很快（Ada 也是如此）。但我们在此特别强调，因为存在一种不幸的、普遍的假设，认为 Ada（因此 SPARK）*不*快。展示 SPARK 代码优于 Rust 代码（对于 `Expand_Key` 来说是显著优于），强化了我们已知的事实：SPARK 除了安全和可靠之外，还是快速的。 ### 证明性能 证明性能分为两个相关部分：获得证明和检查证明。这里我们以相反的顺序呈现，因为检查步骤最可能被重复执行。 #### 检查证明 检查证明所花费的时间，测量于一台 x86_64 Linux 机器上，Intel Xeon 6975P-C，8 个 vCPU（4 核 × 2 线程），15 GB 内存： | 检查 | 结果 | 墙钟时间 | CPU 时间 | 峰值 RSS | 核数 | |---|---|---|---|---|---| | gnatprove，CI 门槛（`check-proof.sh`） | 4085/4085 项检查通过 | 14:02 | 37 分钟 | 485 MB | 8 | | gnatprove，SBox_Entries（`prove-slow.sh`） | 2565/2565 项检查通过 | 15:20 | 25 分钟 | 376 MB | 8 | | FFI（`check-ffi.sh`） | 141 个性质全部通过：36 个穷举，105 个随机 | 8:47 | 9 分钟 | 389 MB | 1 | | SAW，默认（`check-saw.sh`） | 1895 项证明（87 项实现，1808 项规范层）；20/20 个反向控制失败 | 47:16 | 48 分钟 | 2.3 GB | 1 | | SAW，长模式（`SAW_LONG=1`） | 2142 项证明（87 项，2055 项）；20/20 个反向控制失败 | 1:46:49 | — | — | — |