Anthropic称Claude已证明123个库的安全属性

Anthropic于2026年10月22日发表研究称，在与Theorem合作开展的一项研究中，Claude针对123个开源库的239个模糊测试入口点，在RISC-V汇编代码层面生成了经机器验证的安全属性形式化证明。

Anthropic称，Claude修复了发现的漏洞，随后证明，对于小于64 MB的所有输入，以及所有经过建模的Linux操作系统响应和内存布局，程序都将正常退出，不会触发内存安全错误或断言失败。这些证明假设程序以单线程静态二进制文件的形式，在使用Linux的RISC-V CPU上运行，并具有固定的内存预算。Anthropic表示，这些证明共包含约1.8亿行Rocq代码；一项典型证明约有60万行，用于覆盖中位长度为18,000条RISC-V指令的二进制文件。该公司称，据其所知，这是首次大规模尝试利用AI在汇编代码层面为生产软件应用形式化验证。

部分证明及其背后的RISC-V和操作系统语义正在GitHub上发布。Anthropic称，还将公开为该项目构建、此前尚未公开的可信组件，无需修补即可完成证明的模糊测试的完整证明，以及无法证明的模糊测试的规格说明；而可能暴露未修补漏洞的证明则不会公开。

将模糊测试转化为形式化证明

这种方法会将每个库中现有且可编译的模糊测试转化为一份形式化规格说明，其中编码了一条规则：对于任何小于64 MB的输入，测试都不会崩溃。该规格说明以编译后的RISC-V指令为对象，采用Theorem对RISC-V指令集和Linux进程的形式化语义；Rocq证明检查器则会依据规格说明验证每项完成的证明。Anthropic称，这意味着开发者只需信任三个组件：RISC-V和Linux进程的形式化模型、精确的定理陈述，以及Rocq检查器本身。

Anthropic称，该公司将这一流程应用于Google的OSS-Fuzz计划中的数百个项目。该计划为符合条件的开源项目提供持续模糊测试，并使用AddressSanitizer自动检测C和C++程序；每当程序发生内存访问错误时，这款工具都会使其崩溃。日期为2026年10月22日的附录详细列出了所证明的完整定理：对于所有小于64 MiB的输入和所有内存布局，无论是经ASan检测的二进制文件还是未经检测的普通二进制文件，都不会发生故障、异常终止或出现未建模行为；两者产生的读写轨迹、退出行为和最终文件系统状态也完全相同。

附录称，在这项工作中，Claude编写了约10亿行Rocq代码，其中约1.8亿行通过了证明检查器。cJSON中一个391行的解析器入口点对应的证明长达63万行；而链接了51,000行代码的fftw3对应的证明则有48万行。由于Claude获准在完成证明前修补代码，Anthropic称，该公司对补丁施加了惩罚，并对证明补丁改变了哪些输入给予额外奖励，同时记录并审计补丁，以遏制奖励操纵行为。

证明尝试中发现的漏洞

Anthropic报告称，尝试证明的过程中发现了数百个漏洞，其中许多是模糊测试器不太可能发现的。在证明一个库的入口点时，Claude发现解压程序中的计数器发生下溢，导致越界写入，但只有在输入约为20 MB且采用一种罕见的特定布局时才会出现。其他发现还包括：图像解码器中的越界读取，需要64 MB输入和超过2 GB内存；只有在针对同一文件的两个句柄之间按特定顺序调用函数时才会出现的越界读取；以及在libexpat中再次发现的CVE-2026-56132，该漏洞需要深度嵌套的输入才能触发。

Claude还发现了一些不会导致崩溃的逻辑漏洞，包括应用程序可加载文件的限制并非总能得到执行。Anthropic称，该公司在尝试验证若干广泛使用的关键应用程序时，发现了一个此前未知、已潜伏十余年的逻辑漏洞；在验证一款广泛使用的PDF阅读器期间，该公司一周内发现的安全漏洞数量，达到了通常一年内报告的数量。

其他实验与效率发现

除了OSS-Fuzz之外，Anthropic还让Claude为RFC 1950编写形式化规格说明。RFC 1950是一份定义zlib压缩格式的技术文档。随后，Claude证明Linux内核中的zlib实现能够正确实现该规格。Claude直接证明了编译为x86的二进制文件，采用的是由Claude生成的x86指令集形式化语义。Anthropic称，该公司还对另外六个广泛使用的库重复了这一流程，并发现了一些轻微且无法利用的边缘情况漏洞，目前正将这些漏洞提交给上游。该公司还报告称，生成x86语义的过程中发现了官方参考文档中的数百处错误，以及硬件本身少量漏洞；逐条单步执行这些语义，还能在Linux内核上启动Ubuntu用户空间。

在另一项实验中，Claude 用 Rust 为 Python 的一个大子集构建了解释器，并使用 Verus 验证工具证明，该解释器遵循一篇学术论文中阐述的 CPython 语义。技术附录指出，解释器的全部 17 个层级都已得到证明，定理表明：“只要解释器返回结果，该结果就是形式语义所规定的结果。”Anthropic 表示，对 170 万个随机生成的 Python 程序进行实证测试后发现，其中 99.95% 的测试表现出与 CPython 相同的行为；在故意植入的 7 个漏洞中，随机测试未能发现其中 5 个，但这 7 个漏洞都导致证明无法成立。

为衡量效率，Anthropic 将真实的 OSS-Fuzz 入口点缩减，构建了 36 个小型验证任务，生成的程序包含 283–2,491 条指令，输入限制为 64 字节，并以一个约含 100 条指令的“mini-ASan”运行时取代 AddressSanitizer。Anthropic 报告称，Opus 5.5完成一半任务所需的 token 数量，比 Opus 5 少约 40%。Anthropic 还报告称，在共享工作区中允许彼此复制证明的智能体，比单独工作的智能体少用了 17% 的 token；有些智能体此前单独工作时未能成功，之后却完成了任务；而单独工作的智能体有两项证明未能完成。该公司表示，在 OSS-Fuzz 项目中，大规模协作也呈现出同样的复用效应：智能体团队会复制已完成的证明并加以改编，因为每项证明的大部分内容都涉及共享的 C 运行时和 AddressSanitizer 初始化代码。

已说明的局限性与 OSS Verify 计划

Anthropic 指出，这些证明并不意味着相关库不存在漏洞：剩余漏洞可能位于受信任组件之中，也可能超出证明的范围。这些证明适用于链接 musl libc 的单线程静态 RISC-V 二进制文件，而大多数用户在 x86 或 ARM 上运行这些库，并动态链接 glibc；此外，AddressSanitizer 也无法检测所有内存安全漏洞。该公司表示，随着模型改进，这些局限有望变得更容易解决。

Theorem 正通过其 OSS Verify 计划，向符合条件的开源项目免费提供同一套流程。项目可通过提交拉取请求，将 project.yaml、Dockerfile 和 build.sh 文件添加到该计划的代码库中来申请加入；Theorem 表示，其审核项目的方式与 OSS-Fuzz 类似，并优先考虑广泛使用的关键基础设施。据 Theorem 介绍，维护者会获得一份经 Rocq 内核检查的 Rocq 证明，证明每个模糊测试目标在任何不超过 64 MiB 的输入下都不会崩溃；证明过程中发现的漏洞会通过电子邮件私下告知维护者，且没有披露期限；生成证明可能需要数天。Theorem 的路线图计划验证整个 Nix 生态系统，包括 glibc、OpenSSL 和 cURL 等关键基础设施。