全球互联网差点炸了，Claude 甩出 1.8 亿行证明来补窟窿

昨天，全球互联网经历一次大危机。

欧洲政务服务暂停，日本的 pixiv、Niconico 等平台紧急维护，甚至寿司郎都崩了。这次 PHP 漏洞，让多个国家的网站忙着「拔网线」、打补丁。

今天 Anthropic 就甩出一项新成果想要补上这个窟窿：Claude 写出了约 1.8 亿行通过机器检查的数学证明，涉及 123 个开源库中的 239 个测试入口。它要证明的是，程序里的这些地方，在设定条件下，经得住各种输入而不崩溃。

更早公布的另一项工作，已经促成了 OpenSSH 的修复：让 Claude 找出那些本不该对外开放的功能，把检查提前，拦住不该处理的请求。

一项尝试用数学证明代码的安全，另一项已经推动软件改了代码。Anthropic 给出的防守办法，开始有了具体的样子。

图源：Anthropic，形式化验证研究官方配图。

先把不该对外开放的功能关上

一个陌生人连上服务器，发来的数据能触发哪些功能、触碰到哪些代码？

这些可被接触到的部分，就是软件的「攻击面」。

Anthropic 让 Claude 检查了 25 个开源项目，找出 493 项问题：有的功能默认开放，却根本用不上；有的复杂代码跑完了，程序才想起检查身份是否合法；还有一些配置，单独看没问题，放在一起就引发新的安全问题。

这 493 项统计的是不必要的暴露，这里面也有些尚未发现可直接利用的漏洞。提前收紧这些地方，就能减少攻击者接触代码的机会。

图源：Anthropic。三类项目分别为面向公众、需要身份验证和私有使用；

其中一个例子是 OpenSSH，管理员用来远程登录和管理服务器的工具。

管理员明明关掉了一项功能，外面的人却仍能让它运行。

Anthropic 在 OpenSSH 10.4 里发现，问题出在处理顺序上。对方发来一份用于验证身份的密钥，程序先读取、处理其中的数据，最后才检查管理员是否允许使用这种密钥。

但这样为时已晚，即使相关功能没有启用，对方也没有登录，约 4500 行处理新签名算法的代码仍可能被触发。

修复就是把顺序调过来：先检查这种密钥是否允许使用，不允许就拒绝，允许了再交给后面的代码处理。

10 月 6 日发布的 OpenSSH 10.6 已经加入这项改动，比这次 PHP 漏洞公开还早。发布说明要求尽早检查密钥和证书签名的类型，减少禁用算法的暴露，并注明了 Chris Rohlf、Claude 和 Anthropic Research 的参与。

那些原本就不需要的入口，可以在发现具体漏洞之前先关上。

剩下的功能还要继续接收请求、处理文件。Anthropic 的另一项研究，就从这些必须运行的代码入手。

程序会不会崩溃？让 Claude 写证明

程序员圈有个经典段子：测试员走进酒吧，先点一杯啤酒，再点零杯、负一杯、十亿杯，最后点了一只蜥蜴。酒吧都应付过去了，测试通过。

结果，第一位真正的顾客进来问了句「厕所在哪」，酒吧崩溃了。

给程序找漏洞，也得试试那些开发者没想到的输入。比如一个读图程序，正常图片能打开，损坏的呢？文件被截掉一半呢？塞进去一堆随机数据呢？

模糊测试就是把这类尝试自动化，批量生成、修改输入，看哪一种会让程序出错。负责把输入交给指定功能的那段测试程序，就叫「测试入口」，测过的文件再多，仍然可能漏掉某一种恰好让程序出错的组合。

Anthropic 和 Theorem 给 Claude 的任务，是证明一条写明的要求：在规定的运行条件下，指定测试入口无论收到什么输入，只要小于 64 MB，都不会触发所定义的崩溃。

Claude 写出的推导，要交给名叫 Rocq 的工具检查。它会按照形式逻辑规则一步步核对，推导不成立，就通不过，不能用「我检查过，没问题」糊弄。

在一项小规模对照实验里，团队给一个只能运行部分 Python 语法的解释器故意放入 7 个错误。随机测试漏掉了 5 个，而这 7 个错误，每一个都会让证明检查无法通过。

写这样的证明，要花多少工夫？

从研究附录里的 cJSON 案例可以看出一些端倪：一个解析入口只有 391 行，相关证明却有约 63 万行。甚至程序启动、分配内存，这些平时很少被用户留意的过程，也得算进去。

这批证明代码里，超过一半由 Claude 编写的工具自动生成。写完还不算结束，检查一份证明，需要约 30 分钟到数小时的 CPU 时间。

1.8 亿行证明，也有管不到的地方

1.8 亿行证明，听起来足够惊人，那是不是所有漏洞都堵上了？

团队公开了其中 25 个库、60 个入口的证明，OpenSSL、simdjson、zstd 都在清单里。但一个库有许多功能，验证了其中一个入口，还是不能说明整个库都安全了。

官方动画：绿色部分表示在给定条件下获得证明的路径。

这批证明还有明确的运行条件：程序已经编译成机器执行的代码，使用 RISC-V 处理器架构，运行在 Linux 环境里。换成常见的 x86 或 ARM 版本，同一份证明就不能直接拿来用了。

而且，「不崩溃」还有一种让用户高兴不起来的情况：程序一直跑，始终不给结果。当前公开的证明没有排除这种可能。更何况，还有算错结果、内存泄漏等检测器这些没有覆盖的问题。

证明所依据的机器模型，也需要可靠。Theorem 用数学规则描述处理器执行指令、操作系统响应程序的方式，但目前只覆盖 Linux 的一部分行为，并依赖一些假设。真实机器如果出现模型没有描述的行为，证明就管不到那里。

漏洞找到了，为什么没能马上修好

回头看 PHP 的漏洞，有人注意到问题之后，修复仍然卡了很久。

2024 年，开发者修复外部审计发现的问题时，就注意到了内存耗尽处理中的隐患。但当时还没找到明确的远程代码执行路径，几种修法也都不好办：有的会破坏兼容性，有的可能带来新的拒绝服务风险，还有的会牵动大量第三方扩展。

PHP 基金会在复盘中承认，决策流程和资源不足拖延了修复。

网站不能为了修一个问题，把原来能用的功能也改坏了。安全证明要进入日常维护，同样得回答这个问题。

可几十万行证明的工作量，又由谁来承担？

和 Anthropic 合作的 Theorem，这家专门研究如何用数学证明检查软件的公司，想先验证那些被大量软件共同使用的基础组件。

比如，很多软件都依赖 OpenSSL 来处理加密通信。Theorem 分析了 Nix 收录的软件包，发现近 1.6 万个软件包运行时会直接或间接用到它。

如果先完成 OpenSSL 的相关验证，其他项目就有机会沿用这部分证明，再检查自己的代码，省去重复验证同一个组件的工作。Theorem 正计划沿着这个方向推进。

图源：Theorem。这张路线图设想先验证 OpenSSL 等共享组件，让上层软件复用其证明，再验证各自的代码

OpenSSH 维护者的方案更加硬核——加快发版。

他们在 10.6 的发布说明里写了，同一个由 AI 发现的问题，后来又被其他研究者独立找到了。既然研究者能反复找到，攻击者也可能做到。维护者因此决定更频繁地发布更新，让用户尽早拿到修复。

Claude 能帮忙检查代码、写证明，维护者还得决定怎么改，确认旧功能还能用，再把更新交到用户手里。

Anthropic 给出的这些办法，最终也要走完这段路，AI 不是一把万能钥匙。