Anthropic 用 Claude 对 123 个开源库完成汇编级形式化安全证明

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 证明了：在特定假设下（即程序以单线程静态二进制形式运行、内存预算固定、运行在采用 Linux 操作系统的 RISC-V¹ CPU 上），对于所有小于 64 MB 的输入以及所有建模的 Linux 操作系统（OS）响应和内存布局，这些程序将始终正常退出，不会触发内存安全错误或断言失败。这距离修复所有可能的 bug 仍很遥远，但确实让我们比以往更接近目标，并提供了通往该目标的路线图。

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

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

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

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

将测试转化为证明

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

为了针对我们试图证明的开源库代码解决这一问题，我们采取的方法是：自动将其已有的可编译测试套件转换为一份规范，具体做法是把“该测试套件始终通过”这一规则编码进去，并采用一个通用模型来刻画在 Linux 上执行任何 RISC-V 编译二进制文件的含义。从历史上看，证明这类规范一直是难以处理的，原因在于编写一个能够涵盖并论证数万条汇编指令在任意输入下的所有可能行为和交互的证明本身具有内在复杂性（以及由此导致证明往往极其庞大）。这正是当今 LLM 的用武之地：为达成一个定义明确的目标而处理数百万行代码，正是 LLM 极其擅长的事情。

在这个项目中，我们从模糊测试入手。在这类测试中，开发者在其代码中编写一个入口点²来接收输入，任何导致崩溃的输入都是作者所关心的缺陷。随后，模糊测试器这一测试引擎会在该入口点生成海量的半随机和变异输入，以试图发现缺陷（如图 1 所示）。模糊测试器运行的时间越长，能发现的缺陷就越多。但这本质上是一种暴力过程，无论尝试多少输入，都无法保证覆盖每一条可能的代码路径。

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

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

在几周的时间里，Claude 成功修补了它发现的漏洞，随后证明：对于 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 上，以单线程静态二进制形式运行，并具有固定的内存预算。扩大这些证明的范围完全触手可及，因为这将涉及为更多汇编架构和其他操作系统进程标准化语义。请参阅专家对 Claude 所写证明的评论。

尽管证明代码量巨大，但几乎不需要人工审查。Rocq 证明检查器确保证明正确地满足了规范。因此，开发者唯一需要信任的产物是：

• RISC-V 和 Linux 进程的形式化模型；
• 所证明的确切定理陈述；
• Rocq 证明检查器本身。⁵

这并不意味着这些库不包含漏洞。相反，这意味着任何剩余的漏洞要么存在于上述列出的产物中，要么超出了 Claude 证明的范围。加固这些仍可能存在漏洞的可信组件（Rocq、RISC-V 和 Linux 语义）并非易事，但这比调试大规模证明所覆盖的每一行代码要容易得多——尤其是因为这种方法可以在不增加可信组件规模的情况下保护任意数量的项目。

我们欢迎对我们的证明进行独立验证，并鼓励改进我们的方法。为此，我们发布了为本项目制作但尚未公开的可信组件（上述）；Claude 为无需修补的模糊测试提供的完整 Rocq 证明；以及我们无法证明的其他模糊测试的规范。

发现并修复漏洞

上文我们展示了，你可以将许多开源库开发者编写的测试（模糊测试）转化为规范，Claude 可以证明这些规范始终通过，有时需要先修补它发现的剩余漏洞。因此，尝试证明这些规范的过程发现了数百个漏洞。

在 Claude 尝试证明数百个入口点的过程中，出现了大量漏洞。为确保 Claude 不必每次遇到这种情况都停下来等待人工处理，我们让 Claude 修复它发现的漏洞：它修补代码，导致规范随修补后的代码重新生成，然后 Claude 继续证明新的规范。⁶

我们发现的许多 bug 是模糊测试器不太可能找到的。模糊测试器会变异小输入，通常上限为 1 MB，并且通常依赖代码覆盖率来引导它们发现 bug。在证明某个库中的一个入口点时，Claude 在其解压器副本中发现了一个计数器下溢，导致越界写入，但仅在约 20 MB、具有一种罕见特定布局的输入上才会触发。其他 bug 包括：一个图像解码器中的越界读取，需要 64 MB 输入和超过 2 GB 内存；另一个库中的越界读取，需要对同一文件的两个句柄进行特定调用序列；以及在 libexpat 中重新发现 CVE-2026-56132，该漏洞需要深度嵌套的输入。Claude 还发现了根本不会导致崩溃的逻辑 bug。例如，在证明某个库是内存安全的过程中，它注意到一个用于限制应用程序可加载哪些文件的功能并未始终被强制执行。

这个项目的最终目标是获得证明：经 RISC-V 编译的模糊测试已没有剩余的崩溃可被发现。然而，上述这类 bug 表明，无论该目标是否达成，这个过程还有另一个好处：即使只是尝试这个过程，也会产生需要修复的真实 bug。

证明超越内存安全

证明一个模糊测试不再有崩溃可被发现，其意义比听起来更大。在现实世界的代码中，模糊测试常常用于检验有意义的高层属性是否被违反，例如编码-解码往返、幂等性、代数定律、差分测试、自洽性或与参考实现的等价性。例如，针对 LZO 压缩算法的模糊测试断言：如果你压缩一个输入，然后解压它，结果与原始输入相同。如果该属性不成立，程序就会崩溃——因此证明测试永不崩溃，就等同于证明该属性本身。

即使这些属性并非由开发者直接指定，这种情况也可能发生。例如，为了让 Claude 完成针对 cpp-httplib 的 OSS-Fuzz 证明，必须排除因 std::set 析构函数中递归过多而导致栈溢出的可能性。这个递归深度受树的最大深度限制，因此 Claude 必须（在机器码上！）证明 libc++ 的红黑树再平衡算法被正确优化，以保持树的深度在对数范围内有界。

其他形式化验证案例研究

形式化验证是一个广阔的领域。上述从模糊测试到证明的例子，是 LLM 通过直接将证明应用于机器码，使形式化验证更广泛可用的一个实例。

我们还看到在其他方面将 LLM 与形式化验证结合的成功案例。例如，我们让 Claude 为 RFC 1950 编写形式化规范，该技术文档定义了 zlib 压缩文件格式。然后，我们让 Claude 证明 Linux 内核中的 zlib 实现正确实现了该规范。与上述示例一样，Claude 在二进制层面证明了这一性质，只不过这次不是 RISC-V，而是使用 Claude 生成（并经过大量测试）的 x86 ISA 形式化语义，直接证明了 x86 编译的二进制文件。⁷ 随后，我们对另外六个广泛使用的库重复了这一过程。在此过程中，我们在边缘情况中发现了一些轻微（不可利用）的 bug，目前正在向上游提交。我们从这次实践中得出两个结论：(1) 这些经过极其充分测试的代码库已经几乎完全正确；(2) 对真实现有代码库证明端到端正确性性质是可能的。

在另一项实验中，我们让 Claude 用 Rust 开发一个支持大部分 Python 子集的解释器，并证明（使用 Verus，一个 Rust 验证工具）它符合一篇学术论文中概述的 CPython 语义。然后，我们通过运行超过 170 万个随机生成的 Python 程序，实证测量了其对 CPython 行为的符合程度，发现 99.95% 的测试与 CPython 行为完全一致，其余测试差异均为意料之中的已知边缘情况。

我们还通过对简单安全性质的形式化验证尝试，在几个广泛使用且关键的应用中发现了问题。其中一个应用里，我们发现了一个潜伏十多年、此前未知的逻辑 bug。在验证一个广泛使用的 PDF 阅读器的过程中，我们一周内发现的安全 bug 数量相当于通常一年报告的数量。

有关其中部分工作的更多细节，请参阅附录。

这仅仅是开始

LLM 辅助形式化验证的关键限制之一是，证明可能需要消耗数亿个 token。如果我们的目标是让这些方法惠及整个软件生态系统，成本效率就至关重要。幸运的是，有充分理由预期效率会提升。

更新的模型需要更少的 token

我们基于真实的 OSS-Fuzz 代码构建了 36 个小型验证任务。Opus 5.5 证明其中一半任务所用的 token 比 Opus 5 少约 40%。随着模型在长验证任务上接受训练，我们预计这一趋势将持续。

证明可以复用

当智能体各自独立工作时，它们往往会重复大量工作。证明与软件一样，是由更小的证明递归构建而成——而证明越小，往往越容易复用。为了衡量这一点的影响，我们让智能体在证明各自目标时互相复制彼此的证明。在获得这个共享工作区后，智能体所需的 token 比单独工作时减少了 17%，一些智能体甚至在单独尝试失败后取得了成功。

我们在 OSS-Fuzz 证明工作中大规模观察到了同样的现象。证明的大部分内容涉及每个程序都包含的代码（尤其是 C 运行时和 AddressSanitizer 的初始化），因此差异很大的程序最终也可能有大量重叠的证明。智能体团队利用了这一点，复制另一个团队已完成的证明，然后将其适配到自己的程序（图 6）。

证明的这种可复用性正是 Mathlib 得以成长的方式——它是 Lean 中的形式化数学共享库，已发展到由 700 多名贡献者提交的近 300,000 个定理：每个新证明都建立在现有成果之上。我们在 OSS-Fuzz 工作中也积累了类似的证明库，其中一些将包含在我们的发布中（我们不会发布可能暴露开源软件中未修补漏洞的证明）。

随着我们从这些初步实验中逐步推进，我们需要一种策略来验证海量的现有软件，从最关键的依赖项开始。正如我们所展示的，这可以通过使用通用规范和二进制层面的工作大规模实现，从而避免用另一种语言重写整个代码库。

这种方法还促进了包级别粒度的证明复用，这意味着每个依赖项只需验证一次。依赖关系遵循幂律：即使只证明一小部分共享库，也能让大量软件变得可证明。更多细节请参见 Theorem 的路线图，该路线图旨在验证整个 Nix 生态系统，其中包括 glibc、OpenSSL 和 cURL 等关键基础设施。

局限性

在实践中，形式化验证有时对代码安全性的证明可能比我们期望的要少。

“形式化验证”并不意味着“没有缺陷”。Claude 可以编写一个证明，表明编译后程序的行为满足形式化规范的要求（该证明由外部证明检查器验证）。然而，证明检查器无法告诉你你的规范是否与现实相符。要与现实相符，规范必须正确涵盖并建模已验证程序所运行的真实机器的所有方面，包括 CPU 和操作系统。当已验证代码中出现缺陷时，是因为规范或假定的机器语义与现实不同。幸运的是，这也意味着我们知道在哪里寻找剩余缺陷，以及如何设计一个系统来最小化这些仍可能存在缺陷的缺口。以下是这如何适用于我们的证明，以及未来工作如何弥合这些缺口的想法。

真实机器会做出模型未描述的行为。我们的证明针对的是单线程、静态链接到 musl libc 的 RISC-V 二进制文件。然而，大多数人是在 x86 或 ARM 上运行这些库，并将它们动态链接到 glibc。要弥合这一差距，我们需要更接近实际部署系统的系统模型。例如，为 x86 生成精确语义就是朝着这个方向迈出的一步。

该主张可能并未涵盖我们关心的所有内容。我们证明了在 Google OSS-Fuzz 的许多模糊测试入口点上，对于任何小于 64 MB 的输入，崩溃都不会触发，包括 ASan 崩溃。然而，ASan 并不能检测所有内存安全缺陷，而且我们并未验证每个库的所有入口点。即使我们验证了，验证所有入口点也无法覆盖整个库（尤其是在存在死代码的情况下）。此外，真实程序可能误用该库，导致调用方出现内存损坏。要弥合这一差距，我们需要规定调用方对每个公开函数必须做什么，并且调用方必须严格遵守。

我们预计，随着我们对如何利用 LLM 进行形式化方法的研究不断深入，以及模型持续改进，这些局限将变得可控，我们将能够验证我们所依赖代码中更大比例的部分。

结论

趋势很明确：形式化验证过去只在最安全关键的代码中用于定制专家打造的保证，而很快它将像今天的模糊测试一样，对几乎所有生产软件都变得切实可行。就像静态类型、测试框架和其他正确性工具一样，验证将从“外挂式”成熟为“内置式”，这不仅由 LLM 驱动，也由语言设计和开发工作流的创新驱动。

在当今世界——LLM 自动扫描并发现越来越多的代码漏洞——我们必须采用能够保证代码安全属性的流程。LLM 规模化的形式化验证是一种有前景的方法，能够以以前无法达到的范围和规模来确保这些保证。我们鼓励其他人进行实验，以便我们共同构建一个世界：稳健的软件广泛普及，软件缺陷成为被充分理解且可快速处理的罕见现象。

阅读完整附录。