第 01 章：引言

Keane Lucas、Aengus Lynch、Luna Tong、Luke Champine、Zygi Straznickas、Dino Distefano、Harshikaa Agrawal、Evyatar Ben Asher、Ava Howell、Sami Jawhar、Chris Rohlf、Nickolai Zeldovich、Nicholas Carlini、Rajashree Agrawal、Jason Gross

大多数软件都充斥着漏洞，而 AI 现在可以轻易地找到并利用这些漏洞。针对网络攻击的标准防御手段已不再足够：我们需要能够证明代码不存在漏洞的方法。形式化软件验证可以提供这种保证，但它在历史上需要专家数年的努力，对大多数现实项目而言并不实用。然而，在与 Theorem 的合作中，我们表明情况已不再如此：LLM 现在能够大规模生成形式化证明，从而催生出包含可证明安全保障的新软件开发工作流。借助 Claude，我们在超过 100 个真实开源软件库的汇编代码层面（RISC-V）证明了安全属性。据我们所知，这是首次大规模利用 AI 将形式化验证应用于汇编代码层面的生产软件。 在编写证明的过程中，Claude 还发现了多年来一直未被察觉的漏洞，尽管这些项目已经历了数万亿次测试运行。随着模型能力持续提升，我们预计形式化验证将成为安全软件开发中不可或缺的一部分。

引言

即使是成熟且经过大量测试的软件也会包含缺陷，而大语言模型（LLM）在发现这些缺陷方面日益擅长。Linux 内核是当今测试最充分的软件之一，部署在全球数十亿台设备上，最近却有超过 1,000 个漏洞被披露。随着前沿模型越来越有能力将看似无害的缺陷串联成严重漏洞利用，我们需要能够在这些缺陷被野外利用之前检测并修复它们的技术。

理想情况下，这类技术能够找到并修补所有缺陷，然后提供某种证明，说明再也找不到更多缺陷了。形式化验证就是实现这一目标的一种方法。在形式化验证中，开发者将代码转换为数学模型，然后尝试证明它始终遵循某一组定义好的安全规则。如果证明失败，就意味着代码中可能存在违反某条规则的缺陷，而失败的性质暗示了缺陷可能是什么。重复这一过程（每次消除失败原因之后），最终将得出证明：代码中不存在任何会违反这些规则的缺陷。

然而，形式化验证并不容易。证明的规模可能比原始代码大许多倍，编写证明需要大量精力以及小众且高度专业化的技能。例如，实现 seL4 操作系统内核用了两人年，但对其进行形式化验证用了20人年。因此，形式化验证此前只在真正关键的任务应用中才具有可行性，例如空客的航空电子代码。

但 LLM 正在让这件事变得容易得多。前沿模型现在能够完全自主地为真实世界的软件生成正确性证明。为了演示这一点，我们让 Claude 在 123 个开源库中证明有用的安全属性，包括证明其中一些可执行产物在某些条件下永远不会崩溃。具体来说，Claude 证明了这些程序在以下条件下将始终正常退出，不会触发内存安全错误或断言失败：对于每一个小于 64 MB 的输入，以及每一个建模的 Linux 操作系统（OS）响应和内存布局，在特定假设下（即程序作为单线程静态二进制运行，在 RISC-V CPU 上使用 Linux 操作系统，并具有固定的内存预算）。这距离修复所有可能的缺陷仍然很远，但它确实让我们比以前接近得多，并提供了通往这一目标的路线图。

我们正在发布这些证明的一个子集，以便任何人都可以验证和复用它们，同时发布 RISC-V 和操作系统语义。本项目的合作方 Theorem 也提出为其他开源项目运行同一流程，并发布了一个 Claude 技能，帮助开发者开始验证自己的代码。

形式化验证是一个广泛的领域，包含许多方法论。下面，我们还描述了使用其他形式化验证方法来加速其他安全或软件开发任务的初步探索，例如评估 zlib 压缩算法的安全性、证明用 Rust 编写的 Python 解释器的行为等价性，以及根除关键软件中长期存在的缺陷。

形式化验证的前景是光明的。随着模型变得更加智能，编写证明的成本正在下降。此外，随着更多代码被形式化，以及实现安全保障的方法变得更加标准化，跨代码库复用或修改证明的能力将摊薄成本。我们鼓励所有开发者用 LLM 探索形式化验证——尤其是那些以前用能力较弱的模型尝试过并发现行不通的人。

在本文的其余部分，我们将更详细地介绍我们的形式化验证实验。

将测试转化为证明

要证明一段软件是正确的，我们必须首先明确“正确”究竟意味着什么。正确性由规约（spec）来定义。在某些程序中，有一种清晰的方式可以形式化地指明程序的预期行为。例如，一个 PNG 解码器接收一串字节，并（遵循 RFC 2083）将这些字节解码为对应的图像。但对于大多数程序而言，情况并没有这么简单。一个文本编辑器或一个网页浏览器“正确”意味着什么？获得一份全面且无歧义的规约十分困难，这是在大规模范围内验证软件的一大障碍。

为了解决我们想要证明的开源库代码中的这一问题，我们采取的方法是：自动将其既有的可编译测试套件转换为一份规约，具体做法是把“该测试套件始终通过”这条规则编码进去，并使用一个通用模型来描述在 Linux 上执行任何 RISC-V 编译二进制文件意味着什么。从历史上看，证明这类规约是极其困难的，因为编写一个证明本身就固有地复杂：它要涵盖并论证数万条汇编指令在任意输入下的所有可能行为和交互（而且由此产生的证明往往极其庞大）。这正是当今 LLM 的用武之地：为了一个明确定义的目标而处理数百万行代码，正是 LLM 极其擅长的事情。

在这个项目中，我们从模糊测试（fuzz test）开始。在这类测试中，开发者在自己的代码中编写一个入口点（entry point）来接收输入，使得任何导致崩溃的输入都是作者所关心的 bug。然后，模糊测试器（fuzzer），即一个测试引擎，会在入口点生成海量半随机且经过变异的输入，试图找出 bug（如图 1 所示）。模糊测试器运行的时间越长，它能找到的 bug 就越多。但这本质上是一个暴力过程，无论你尝试多少输入，都无法保证覆盖每一条可能的代码路径。

为了找出模糊测试本会暴露的所有 bug，我们将模糊测试转化为一份定义在编译后的 RISC-V 指令之上的规约。该规约表示：对于任何小于 64 MB 的输入，模糊测试都不会崩溃。如果 Claude 能够证明这份规约，那么在 RISC-V 上进行的模糊测试就变得多余了：对该入口点进行模糊测试将永远找不到任何 bug。

我们在 Google OSS-Fuzz 计划中的数百个项目中做到了这一点，该计划为符合条件的开源项目提供持续模糊测试。OSS-Fuzz 包含数千个由开发者编写的入口点，它们通过崩溃（例如断言失败时）来查找损坏的代码属性。OSS-Fuzz 会自动为 C 和 C++ 程序插桩 AddressSanitizer（ASan），使得程序在内存被不当访问时崩溃（这是软件漏洞的一个主要原因）。像内存安全这样的广谱规约几乎适用于所有软件。

在几周的时间里，Claude 成功修补了它发现的 bug，然后证明了在 123 个不同的 OSS-Fuzz 库中的 239 个入口点上，对任何输入（最大 64 MB）都不会发生崩溃。 这些证明作用于编译后的 RISC-V 指令（即可执行二进制文件），它们合计约 1.8 亿行 Rocq 代码，其中一份典型的证明约有 60 万行，为二进制文件提供安全保障，而这些二进制文件的中位长度为 18,000 条 RISC-V 指令。这些证明是通过使用 Theorem 的 RISC-V 指令与 Linux 进程语义，将 RISC-V 汇编代码转换为数学模型而构建的。这意味着这些证明目前假设程序在 Linux 操作系统上、以单线程静态二进制形式在 RISC-V CPU 上运行，且具有固定的内存预算。