返回博客首页
Claude 写出 1.8 亿行证明：形式化验证到底证明了什么？
“1.8 亿行证明”很容易让人误以为某个模型已经证明互联网软件没有漏洞。软件团队真正需要回答的问题更窄：证明的是哪个可执行程序、什么性质、哪些输入和系统条件；在生产环境里，还需要哪些安全措施？本文把 Anthropic 的形式化验证研究与其攻击面缩减研究放进一条工程决策链，给安全工程师、开源维护者和技术负责人一套能复核的阅读与试点方法。
两项研究发表于不同日期，目标也不同。形式化验证试图对特定二进制程序在特定模型和前提下不会崩溃给出机器可检查的证明；攻击面缩减寻找不必要的代码可达路径，让攻击者更难触及潜在缺陷。前者不是“所有漏洞清零”，后者也不是“已经证实每一条路径都有漏洞”。把它们混为一谈，会让团队误配预算、误解风险。
先把三组数字放回各自语境
Anthropic 报告：研究团队在 123 个 OSS-Fuzz 开源库的 239 个入口点上，生成约 1.8 亿行 Rocq 证明。这些证明针对编译后的 RISC-V 指令，而不是笼统针对所有平台的源代码；在论文所述假设下，入口点对不超过 64 MB 的输入不会因内存安全错误或断言失败而崩溃。团队还表示先修复了发现的相关缺陷，再对修补后的程序证明性质。
“239”是被验证的入口点，不是 239 个完整产品；“123”是库数量，不等于互联网基础设施覆盖率；“1.8 亿行”是证明脚本体量，不是模型写出的业务代码行数。行数大说明自动化规模，也提醒维护者需要依赖证明检查器，而不是人工逐行阅读。判断实际价值要看定理陈述、可信基础、编译对象和复现材料。
图 1：研究图示中的模糊测试不断尝试具体输入，仍可能漏掉路径；下文的形式化证明转而对指定入口点的全部合规输入作命题。
另一项研究在 25 个项目中记录了 493 个攻击面相关问题。这个数字是研究团队按其方法归类的发现总数，并非 493 个可利用 CVE。它包括默认配置下不必要的预认证可达代码、认证前执行或记录状态的路径，以及配置组合削弱控制等情况。需要逐项复核严重程度、触发条件和修复状态，不能拿总数直接当漏洞排行榜。
证明链条具体怎么工作
形式化验证不是让模型说一句“我检查过了”。研究使用现成的 OSS-Fuzz 测试入口，把开源库和对应测试程序编译成 RISC-V 可执行文件；再结合 RISC-V 指令和 Linux 进程语义，把“正常退出、不触发指定错误”形式化成待证命题。Claude 负责构造 Rocq 证明，Rocq 内核负责检查证明是否满足命题。一个无效的推导即使写得很长，也不会因为语言流畅而通过内核。
这个设计有一个重要优点：模型可以写出大量繁琐推导，最终是否成立由相对小得多、可审查的检查器判断。团队公开了部分证明和可信语义材料，便于外部研究者独立检查。但“内核接受证明”只说明证明与给定语义、定理和被验证对象一致；如果定理写错了、模型对操作系统的抽象漏掉重要行为，或生产系统运行的不是该二进制，结论就不能直接迁移。
图 2：研究展示了组件之间可复用的证明关系；这种共享依赖并不改变逐项核对指令语义、定理陈述与检查器的必要性。
Anthropic 明确列出的运行前提包括：单线程、静态二进制、固定内存预算、RISC-V CPU 和被建模的 Linux 操作系统响应。输入上限为 64 MB。这里的“所有输入”必须读成“在这些前提与该入口点下、尺寸不超过上限的所有输入”。有动态链接、并发、不同架构、未建模的系统调用或更大输入时，需要新的模型和证明，不能自动沿用当前结论。
还有一个容易被忽略的细节：研究中 Claude 可以先修改程序以修复可导致崩溃的缺陷，再证明修改后的版本。因而团队在部署前不仅要保存“证明通过”结果，还要审阅补丁差异、确认行为兼容，并核对上线构建与被证明构建的哈希一致。否则模型可能通过删掉有问题的业务路径来满足过窄定理，却改变了用户真正需要的功能。
“不崩溃”与“安全”之间还有多远
不会崩溃是一项有价值的性质，尤其适用于解析器、解码器和边界复杂的库；但一个程序可能不崩溃，仍然泄露数据、绕过认证、给出错误结果或被滥用计算资源。形式化证明只覆盖定理写进去的性质。不能因一条 no-crash 定理成立，就宣布它没有逻辑错误、侧信道、供应链问题或平台配置风险。
看研究结果时可以做三层核对。第一层是对象：入口点是什么，输入来自哪里，二进制是哪一次构建？第二层是性质：定理是否只检查崩溃，还是也涵盖授权、保密性和业务不变量？第三层是环境：CPU、操作系统、线程、内存预算、外部服务与生产是否一致。任何一层不匹配，都需要说明“仍未覆盖什么”，而不是在演示里缩写成“已证明安全”。
图 3：证明检查器能拒绝无效推导；超出命题范围的业务错误仍需测试、审计和运行时控制。
研究同时提示了成本。复杂证明可能耗费数亿 token，且失败尝试、修复与复核也需要计算和工程人力。对普通业务服务而言，把全部代码一次性送去形式化验证未必划算；从高风险、边界明确、可稳定复现的解析入口开始，更容易得出有用结论。
OpenSSH 案例讲的是“可达性”，不是新 CVE
在攻击面研究中，Claude 跟踪了 OpenSSH 10.4 的 sshd 输入路径，发现约 4,500 行与 ML-DSA-44 签名有关的实验代码，即便算法未启用，未认证客户端仍可进入其中一部分解析和校验路径。研究说明：最初的检查在解析之后；10.5 将检查前移，但后续还发现声明算法与实际编码类型不一致，以及证书 CA 签名路径等缺口。维护者协作后的修复进入 10.6，先按配置允许列表核对，再进入相应解析或签名验证。
这不是说 ML-DSA 算法本身有已证实的漏洞，也不是说任何人都能利用这些代码。真正的工程观察是：没有业务必要的预认证复杂代码不应被默认送到攻击者可触达的路径上。即使没有找到具体缺陷，减少可达代码仍能降低未来未知缺陷的暴露面。团队报告该修复移除了默认构建中约五分之一此前可被未认证客户端触达的代码；数字对应研究的代码可达性分析，不代表风险恰好降低五分之一。
图 4：不同问题类别的数量说明审计需要逐类处理；汇总数字不能直接当成漏洞严重度。
对自己系统做同类检查，可先选一条外部输入到敏感解析器的路径：HTTP 请求进入鉴权前、插件加载前、反序列化前，或者数据库协议解析前。画出“外部输入→类型识别→权限核对→解析/执行”的顺序，问一句：配置明确禁用的功能，其解析器是否仍会被调用？如果答案可能是“会”，再用代码跟踪与可复现测试确认，而不是直接下安全结论。
团队怎样用七天做一个小试点
第 1 天选边界明确的目标：例如公开图片解析库的一条 fuzz 入口，或一个服务的预认证协议解析路径。写出待验证性质和生产风险，不以“试试看 AI 多强”作为唯一目标。第 2 天冻结构建：记录仓库提交、编译器、依赖、编译参数与二进制哈希，让后面的证明指向唯一对象。
第 3 天准备基线：先运行已有单测、模糊测试和静态分析，记录已知崩溃、覆盖范围和未修复问题。形式化验证可以与它们互补，但若连现有测试入口都不稳定，证明工程会被环境噪声淹没。第 4 天列可信基础：CPU 与 OS 语义从哪里来、证明检查器版本是什么、定理如何由团队审查。把这些资料和结果一起存档。
第 5 天运行一个窄任务：只证明一个入口点在指定输入上限与系统模型下不崩溃；或者只审计一个预认证路径中配置禁用代码的可达性。遇到模型建议补丁，先拆分“使性质成立的修改”和“改变功能的修改”，要求每一处都有测试。第 6 天请另一名维护者复核：重新检查定理是否足够强、构建是否相同、补丁是否会造成行为倒退。第 7 天出试点报告，分成“已证明”“已测试但未证明”“未覆盖”“需人工决策”四栏。
一个可复制的试点验收模板如下：
| 栏目 | 必填内容 | 退回条件 |
|---|---|---|
| 被验证对象 | commit、构建参数、二进制哈希、入口点 | 无法复现同一构建 |
| 定理 | 精确性质、输入上限、运行假设 | 只有“安全”这类口号 |
| 可信基础 | 语义模型、检查器与版本 | 关键模型来源不明 |
| 修复变更 | 补丁、回归测试、行为差异 | 为过证明而删功能 |
| 生产适配 | 与线上架构、线程、OS 的差异 | 直接把 RISC-V 结论贴给其他平台 |
| 运营成本 | token、计算、人工复核、持续维护 | 只算首次模型调用 |
若团队使用 Code0 或 Claude Code 做审计协作，可以把定理、测试失败、补丁和复核评论分为不同任务记录，避免 Agent 在同一会话里既写补丁又给自己批准。若通过 Apito 等接入层调用模型，应保存可追溯的请求与费用记录，并把源码、漏洞详情和密钥限定在授权范围内。接口层不会自动保证证明正确；最终仍以检查器输出和独立复核为准。
何时值得投入，何时先做简单的防护
适合优先验证的场景通常具备三个特点：外部输入可触达、失败后果高、性质可以写得窄而清楚。媒体解析器、加密协议实现、文件格式处理和关键认证前路径符合这个方向。若系统以大量第三方服务、动态配置和人工操作为主，先做权限最小化、输入限制、模糊测试、补丁管理和回滚演练，可能比追逐“全系统证明”更快降低风险。
形式化验证与攻击面缩减也有先后关系：先把不必要的路径关掉，再对仍必须暴露的高风险入口证明关键性质，能减少证明范围和维护负担。但缩减后的代码仍需兼容测试；证明过的代码也仍需限制权限。读研究报告时把二者作为可组合的工程手段，别把一篇论文的数字变成生产环境的免责条款。
最后的发布或采购判断应落在证据上：证明脚本能否独立检查，定理是否覆盖目标风险，修复是否合入生产版本，构建哈希是否匹配，运行条件是否一致，成本是否可持续。只要这六个问题有一个答不上来，“已验证”就只能写在研究笔记里，不能写成对外安全保证。
在 Code0 开发流程里怎样保存验证证据
把被证明的提交与二进制哈希、定理文本、检查日志、模型提出的补丁分别作为可追溯工件，而不是只保存 Agent 的总结。每次合并请求让另一名维护者核对‘证明的版本’与‘将要上线的版本’是否一致；构建参数变化就标记旧证明待重新评估。这样审计记录能回答具体版本能保证什么，不会因模型的一句‘已通过’掩盖环境差异。
资料来源
常见问题（FAQ）
1.8 亿行证明是否意味着 123 个库完全没有漏洞？
不意味着。研究证明的是特定入口点、特定二进制、输入上限和系统模型下的 no-crash 性质。未写入定理的授权、数据泄露、逻辑错误和生产环境差异仍需单独评估。
Rocq 检查通过后，还需要人工代码审查吗？
需要。Rocq 检查证明是否满足给定定理；人要审查定理是不是想要的安全性质、语义模型是否可信、补丁有没有改变功能，以及上线构建是否与被验证对象一致。
OpenSSH 案例是否说明 ML-DSA 已被攻破？
不说明。研究描述的是未启用算法时仍存在不必要的预认证代码可达路径，维护者通过提前按配置核对来缩小攻击面；不能据此推断算法被破解或存在可利用漏洞。
我的服务不是 RISC-V，还能直接复用这些证明吗？
不能直接复用针对 RISC-V 二进制的结论。需要相应架构和操作系统语义，并对目标构建重新生成、检查证明；可借鉴的是验证流程与边界记录方法。
安全团队资源有限，先做哪一步？
先盘点外部可达入口和默认启用功能，关闭不必要路径；随后用测试和模糊测试建立基线。只有高风险且边界清楚的入口，才优先做形式化验证试点。
