Anthropic 称 Claude 123个图书馆的安全属性

AI 模型和平台

Anthropic 称 Claude 123个图书馆的安全属性

在 Google 上的首选来源中添加 Unite.AI

Anthropic于2026年10月22日发表研究成果，报告称Claude与定理公司合作，为123个开源库的239个绒毛测试切入点在RISC-V编组码级别上生产了机器检查的安全属性正式证明。

根据Anthropic,Claude补丁了它发现的bug，然后证明程序总是会正常退出而不会触发内存安全错误或失败的断言，对于64 MB以下的每一个输入以及每个模型化的Linux操作系统响应和内存布局。 证明文件假设程序运行为单线的静态二进制，在使用Linux的RISC-V CPU上有固定的内存预算。 Anthropic 称的证明包含约1.8亿行的Rocq，典型的证明运行约60万行以覆盖二进制，中间长度为1.8万RISC-V指令。 称公司，据其所知，这是首次大规模使用AI对组装代码级别的生产软件进行正式核查。

正在GitHub上发布一个子集的证明以及后面的RISC-V和操作系统语义。 Anthropic 称还释放了为项目建造的尚未公开的可信部件，不需要补丁的模糊测试的完整证明，以及它无法证明的模糊测试的规格，同时扣载可以揭示未补丁错误的证明。

将模糊测试输入正式证据

这种方法将每个库现有的可编译模糊测试转换成一个正式的规格编码规则：测试永远不会崩溃64 MB以下的任何输入。 规格在编译的RISC-V指令之上使用RISC-V指令集和Linux流程的定理形式语义来定义，Rocq校验器根据规格验证每个完成的证明。 Anthropic 称这只留下三个组件开发者需要信任：RISC-V和Linux进程的正式模型，精确的定理语句，以及Rocq检查器本身。

Anthropic 称将这个过程应用到Google的OSS-Fuzz倡议的数百个项目中，该举措提供持续模糊测试，用于对开源项目进行资格审查，并自动将仪器C和C++程序与地址Sanitizer(地址Sanitizer)一起使用，这个工具在不适当地访问内存时会崩溃一个程序。 一份日期为2026年10月22日的附录详细说明了完整的定理：对于64 MiB 下的所有输入和所有的内存布局，无论是ASan-instrumented binary还是平面二进制断层，流产，还是展示未建模的行为，都会产生相同的读写痕迹，退出行为，以及最终的文件系统状态。

附录指出，Claude在努力期间写下了约10亿条罗克线，其中约1.8亿条线路通过了校验；cJSON的391线剖析器入口点得到了63万条线路的校验，而fftw3，其中连接的51 000条线路收到了48万条线路的校验。 因为Claude获准在完成证明前补丁代码，Anthropic 称它惩罚补丁，提供额外信用证明输入的补丁更改，以及登录和审核补丁以阻止奖励黑客。

在尝试中发现的臭虫

Anthropic报道说，尝试这些证据会浮出数百个bug，其中许多是模糊的，不太可能找到。 Claude在证明一个库的切入点的同时，在解压器中发现了一个逆向下流，导致出局的写法，但只针对约20 MB的输入，有一个罕见的具体布局。 其他发现包括一个在图像解码器中读取的需要64 MB输入和超过2 GB内存的外传，一个读取的外传需要两个手柄对同一文件进行特定顺序的呼叫，以及一个在libexpat中重新发现CVE-2026-56132，这需要深度的嵌入输入。

Claude还发现了永不崩溃的逻辑错误，包括一个限制，一个应用程序可以加载的文件并不总是被强制的。 Anthropic 称对几个广泛使用的关键应用程序的验证尝试发现了一个以前未知的逻辑错误，这个逻辑错误潜伏了十多年，在验证一个广泛使用的PDF阅读器的过程中，它发现一周内的安全错误与一年中通常报道的一样多。

其他实验和效率调查结果

在OSS-Fuzz之外，Anthropic要求Claude写下RFC 1950的正式规格，即定义zlib压缩格式的技术文件，然后证明Linux内核的zlib执行是正确的。 Claude直接证明了x86编译的二进制，使用X86指令集的Claude生成的正式语义，Anthropic 称它重复了半打其他被广泛使用的库的过程，发现了正在上游存档的小，不可探索的角箱错误。 该公司还报告称，生成x86语义识别出官方参考文献中数百个错误和硬件本身中数量较少的bug，单步通过语义可以启动Linux内核上的Ubuntu用户空间。

在另一个实验中，Claude为Rust中的一大子集Python建立了解释器，并利用Verus验证工具证明它坚持了学术论文中概述的CPython语义。 技术附录指出，所有17级口译员都得到了证明，定理认为“每当口译员返回结果时，结果就是正式语义规定的结果。” Anthropic 称经验测试超过170万随机生成的Python程序在99.95%的测试中发现行为与CPython完全相同；在7个故意注射的bug中，5个幸存了随机测试，而所有7个都打破了证明。

为了衡量效率，Anthropic设计了36项小型核查任务，缩小了真正的OSS-Fuzz进入点，生产了283-2,491个程序指令，其输入量限于64字节，地址安全器被大约100个指令的 " Mini-Asan " 运行时间所取代。 Anthropic报告说，Opus 5.5用比Opus 5.少约40%的代币来证明一半的任务。 Anthropic还报告说，agents允许在共享的工作空间复制对方的证明需要比agents单独工作少17%的代币，有些人在之前的独奏失败后成功，agents单独工作未能完成两个证明。 同样的称公司在OSS-Fuzz工作期间出现了规模化的再利用效果，agent团队复制了完成的证明并进行了修改，因为每个证明大多涵盖共享的C运行时间和地址Sanitizer初始化代码。

说明的限制和开放源码软件核查方案

Anthropic表示，证明并不意味着库是无臭虫的：剩余的bug可能存在于可信任的组件或证明范围之外。 证明覆盖了针对musl libc链接的单线性静态RISC-V二进制，而大多数用户在x86或ARM上运行这些库，并动态链接到glibc上，地址Sanitizer没有检测到所有的内存安全错误。 称公司预计这些限制随着模型的改进而变得可拉动。

定理提供同样的管道，以便通过其开放源码软件核查程序，对开源项目进行免费审查。 通过拉动工程工程请求新增工程。 Yaml, Dockerfile，和建立.sh文件到程序的仓库，和定理称，它按照类似OSS-Fuzz的思路审查项目，根据定理，维护者收到Rocq的证明，经过Rocq内核的检查，每个模糊目标不会在任何输入上崩溃，最高不超过64 MiB；在证明努力中发现的bug通过电子邮件私下向维护者披露，没有披露的最后期限，证明需要多天才能产生。 OpenSSL 和 cURL 等关键基础设施。

本文由 AI图鉴自动抓取并翻译，版权归原作者所有；如需查看原文请点下方链接。

AI Models & Platforms

Anthropic Says Claude Proved Security Properties Across 123 Libraries

Add Unite.AI to your preferred sources on Google

Anthropic published research on October 22, 2026, reporting that Claude produced machine-checked formal proofs of security properties at the RISC-V assembly code level for 239 fuzz-test entry points across 123 open-source libraries, in a collaboration with Theorem.

According to Anthropic, Claude patched the bugs it found and then proved the programs will always exit normally without triggering memory-safety errors or failing assertions, for every input under 64 MB and every modeled Linux operating system response and memory layout. The proofs assume the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V CPU using Linux. Anthropic said the proofs comprise about 180 million lines of Rocq, with a typical proof running about 600,000 lines to cover binaries with a median length of 18,000 RISC-V instructions. The company said that, to its knowledge, this is the first large-scale effort to use AI to apply formal verification to production software at the assembly code level.

A subset of the proofs, along with the RISC-V and operating-system semantics behind them, is being published on GitHub. Anthropic said it is also releasing the trusted components built for the project that are not already public, complete proofs for fuzz tests that required no patching, and specifications for fuzz tests it could not prove, while withholding proofs that could reveal an unpatched bug.

Turning Fuzz Tests Into Formal Proofs

The approach converts each library’s existing compilable fuzz test into a formal specification encoding one rule: the test never crashes for any input under 64 MB. The specification is defined over compiled RISC-V instructions using Theorem’s formal semantics of the RISC-V instruction set and Linux processes, and the Rocq proof checker verifies each finished proof against the specification. Anthropic says this leaves only three components developers need to trust: the formal models of RISC-V and Linux processes, the exact theorem statements, and the Rocq checker itself.

Anthropic said it applied this process to hundreds of projects in Google’s OSS-Fuzz initiative, which provides continuous fuzz testing for qualifying open-source projects and automatically instruments C and C++ programs with AddressSanitizer, a tool that crashes a program whenever memory is accessed improperly. An appendix dated October 22, 2026, spells out the full theorem proved: for all inputs under 64 MiB and all memory layouts, neither the ASan-instrumented binary nor the plain binary faults, aborts, or exhibits unmodeled behavior, and both produce identical read and write traces, exit behavior, and final file-system state.

The appendix states that Claude wrote around one billion lines of Rocq during the effort, of which about 180 million lines passed the proof checker; cJSON’s 391-line parser entry point received a 630,000-line proof, while fftw3, with 51,000 lines linked in, received a 480,000-line proof. Because Claude was permitted to patch code before completing a proof, Anthropic said it penalized patches, offered extra credit for proving which inputs a patch changed, and logged and audited patches to discourage reward hacking.

Bugs Discovered During Proof Attempts

Anthropic reports that attempting the proofs surfaced hundreds of bugs, many of them ones a fuzzer would be unlikely to find. While proving one library’s entry point, Claude found a counter underflow in a decompressor that caused an out-of-bounds write, but only on inputs of around 20 MB with one rare, specific layout. Other finds included an out-of-bounds read in an image decoder requiring a 64 MB input and more than 2 GB of memory, an out-of-bounds read requiring a particular sequence of calls across two handles to the same file, and a rediscovery of CVE-2026-56132 in libexpat, which required deeply nested input.

Claude also found logic bugs that never crash, including a restriction on which files an application can load that is not always enforced. Anthropic said verification attempts on several widely used critical applications uncovered a previously unknown logic bug that had been latent for more than a decade, and that during an effort to verify a widely used PDF reader, it found as many security bugs in one week as are typically reported in a year.

Additional Experiments and Efficiency Findings

Beyond OSS-Fuzz, Anthropic asked Claude to write a formal specification of RFC 1950, the technical document defining the zlib compression format, and then prove that the Linux kernel’s zlib implementation correctly implements it. Claude proved the x86-compiled binary directly, using Claude-generated formal semantics of the x86 instruction set, and Anthropic said it repeated the process for half a dozen other widely used libraries, finding minor, unexploitable corner-case bugs that are being filed upstream. The company also reported that generating the x86 semantics identified hundreds of mistakes in official reference documentation and a smaller number of bugs in the hardware itself, and that single-stepping through the semantics can boot an Ubuntu userspace on a Linux kernel.

In another experiment, Claude built an interpreter for a large subset of Python in Rust and proved, using the Verus verification tool, that it adheres to the CPython semantics outlined in an academic paper. The technical appendix states that all 17 tiers of the interpreter were proved, with the theorem holding that “Whenever the interpreter returns a result, that result is the one the formal semantics prescribes.” Anthropic said empirical testing over 1.7 million randomly generated Python programs found behavior identical to CPython in 99.95% of tests; of seven deliberately injected bugs, five survived random testing while all seven broke the proof.

To measure efficiency, Anthropic built 36 small verification tasks by shrinking real OSS-Fuzz entry points, producing programs of 283–2,491 instructions with inputs limited to 64 bytes and AddressSanitizer replaced by a “mini-ASan” runtime of about 100 instructions. Anthropic reports that Opus 5.5 proves half of the tasks with about 40% fewer tokens than Opus 5. Anthropic also reports that agents allowed to copy each other’s proofs in a shared workspace needed 17% fewer tokens than agents working alone, that some succeeded after previously failing solo, and that agents working alone failed to complete two of the proofs. The company said the same reuse effect appeared at scale during the OSS-Fuzz effort, where agent teams copied finished proofs and adapted them because much of each proof covers shared C runtime and AddressSanitizer initialization code.

Stated Limitations and the OSS Verify Program

Anthropic states that the proofs do not mean the libraries are bug-free: remaining bugs could lie within the trusted components or outside the proofs’ scope. The proofs cover single-threaded static RISC-V binaries linked against musl libc, while most users run these libraries on x86 or ARM and dynamically link against glibc, and AddressSanitizer does not detect all memory-safety bugs. The company said it expects these limitations to become tractable as models improve.

Theorem is offering the same pipeline to qualifying open-source projects for free through its OSS Verify program. Enrollment works by pull request that adds project.yaml, Dockerfile, and build.sh files to the program’s repository, and Theorem says it reviews projects along lines similar to OSS-Fuzz, prioritizing widely used critical infrastructure. According to Theorem, maintainers receive a Rocq proof, checked by the Rocq kernel, that each fuzz target does not crash on any input up to 64 MiB; bugs found during the proof effort are privately disclosed to maintainers by email with no disclosure deadline, and proofs can take multiple days to produce. Theorem’s roadmap targets verifying the entirety of the Nix ecosystem, including critical infrastructure such as glibc, OpenSSL, and cURL.

Auto-fetched and translated by AI Atlas. All rights belong to the original author.