昨日，全球互联网遭遇重大安全危机。欧洲政务服务停摆，日本 Pixiv、Niconico 等平台紧急维护，甚至连锁餐饮品牌寿司郎系统也出现故障。此次由 PHP 漏洞引发的动荡，迫使多国网站采取断网或打补丁等应急措施。
就在行业忙于补救之际，Anthropic 发布了一项旨在从根源上解决代码安全隐患的新成果：利用 Claude 生成了约 1.8 亿行通过机器检查的数学证明，覆盖 123 个开源库中的 239 个测试入口。其核心目标是验证程序在设定条件下，能够抵御各类异常输入而不崩溃。
此外，Anthropic 早前的一项工作已直接促成了 OpenSSH 的安全修复：通过识别并关闭不应对外开放的功能，将安全检查前置，从而拦截非法请求。从理论证明到实际代码修复，Anthropic 提出的软件防御方案正逐渐清晰。
图源：Anthropic，形式化验证研究官方配图。
收缩攻击面：关闭不必要的开放功能
软件的「攻击面」指的是外部用户能够接触到的功能和代码部分。Anthropic 对 25 个开源项目进行了审查，发现了 493 项非必要暴露问题，包括默认开启但无用的功能、身份验证滞后以及配置冲突引发的新风险。提前收敛这些暴露面，可有效降低被攻击的概率。
图源：Anthropic。三类项目分别为面向公众、需要身份验证和私有使用；
OpenSSH 逻辑顺序修复案例
以远程管理工具 OpenSSH 为例，Anthropic 在其 10.4 版本中发现了一个逻辑缺陷：程序在处理用于验证身份的密钥时，先读取和处理数据，最后才检查管理员是否允许使用该密钥类型。这意味着即使相关功能已被禁用，攻击者仍可能触发约 4500 行处理新签名算法的代码。
修复方案是将检查顺序前置：先验证密钥类型是否被允许，若不允许则直接拒绝，不再进入后续处理流程。这一改动已包含在 10 月 6 日发布的 OpenSSH 10.6 版本中，早于本次 PHP 漏洞曝光时间。发布说明明确标注了 Chris Rohlf、Claude 和 Anthropic Research 的贡献，强调尽早检查密钥和证书签名类型以减少暴露。
通过关闭原本就不需要的入口，可以在具体漏洞被发现前消除潜在风险。而对于必须保留的功能，则需要更深层次的验证。
形式化验证：用数学证明代码不会崩溃
传统测试往往难以覆盖所有极端情况。例如，一个读图程序可能能打开正常图片，却在面对损坏文件或被截断的数据时崩溃。模糊测试虽能自动化生成异常输入，但仍可能遗漏特定组合。
Anthropic 与合作伙伴 Theorem 赋予 Claude 的任务是进行形式化验证：证明在指定运行条件下，无论收到何种小于 64 MB 的输入，指定测试入口都不会触发定义的崩溃。推导过程需经由名为 Rocq 的工具严格检查，确保符合形式逻辑规则，杜绝主观判断。
在小规模对照实验中，团队在一个仅支持部分 Python语法的解释器中植入 7 个错误。随机测试漏掉了其中 5 个，但形式化证明成功识别出所有 7 个错误，导致验证无法通过。
高昂的计算成本与代码量
形式化验证的工作量巨大。以 cJSON 案例为例，391 行的解析入口代码对应约 63 万行的证明代码，涵盖了内存分配等底层细节。目前，超过一半的证明代码由 Claude 自动化工具生成，但验证一份证明仍需消耗 30 分钟至数小时的 CPU 时间。
当前局限性与未来路径
尽管 1.8 亿行证明令人瞩目，但其覆盖面仍有局限。目前公开的证明仅涉及 OpenSSL、simdjson、zstd 等库的部分入口，且依赖于特定的运行环境：RISC-V 处理器架构、Linux 操作系统及编译后的机器码。若切换至 x86 或 ARM 架构，证明需重新生成。
官方动画：绿色部分表示在给定条件下获得证明的路径。
此外，「不崩溃」并不等同于完全安全。程序可能陷入无限循环而不返回结果，或存在计算错误、内存泄漏等问题，这些均未在当前证明范围内。同时，验证依赖的机器模型基于假设，若真实硬件行为超出模型描述，证明将失效。
为何漏洞修复往往滞后？
回顾 PHP 漏洞，开发者早在 2024 年就发现了内存耗尽处理的隐患，但因缺乏明确的远程代码执行路径，且修复方案可能破坏兼容性或引发新的拒绝服务风险，导致修复决策拖延。PHP 基金会承认，资源不足和决策流程复杂是主要原因。
安全证明若要融入日常维护，同样面临权衡：如何在不破坏原有功能的前提下提升安全性，以及由谁承担巨大的验证工作量。
复用基础组件验证成果
Theorem 公司主张优先验证被广泛使用的基础组件。例如，近 1.6 万个 Nix 软件包依赖 OpenSSL。若完成 OpenSSL 的验证，上层软件可复用该证明，仅需关注自身代码，从而避免重复劳动。
图源：Theorem。这张路线图设想先验证 OpenSSL 等共享组件，让上层软件复用其证明，再验证各自的代码
与此同时，OpenSSH 维护者采取了更频繁的发布策略。鉴于 AI 和其他研究者能反复发现同一类问题，攻击者也可能做到，因此加速更新成为降低风险的有效手段。
Claude 虽能辅助代码检查和证明生成，但最终的决定权、兼容性确认及更新交付仍取决于人类维护者。AI 是强大的辅助工具，而非解决所有安全问题的万能钥匙。