全球互联网差点炸了，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 都在清单里。但一个库有许多功能，验证了其中一个入口，还是不能说明整个库都安全了。 官方动画：绿色部分表示在给定条件下获得证明的路径。 这批证明还有明确的运行条件：程序已经编译成机器执行的代码，使用