北京
10月23日消息，近日，Anthropic 前沿红队联合 Theorem Labs 发布最新研究报告，利用 Claude 大模型对底层 RISC‑V 汇编开展大规模形式化验证，几周时间完成 123 个开源代码库、239 个测试入口验证，生成1.8 亿行可通过机器核验的 Rocq 数学证明代码，挖掘出大量传统测试手段无法发现的软件漏洞，甚至定位到 x86 处理器硬件层面缺陷。
传统安全领域广泛使用谷歌 OSS‑Fuzz 模糊测试，通过海量随机输入轰击程序寻找崩溃问题，累计完成上万亿次测试。但模糊测试属于概率性测试，输入存在大小限制，部分罕见路径很难被覆盖，不少高危漏洞会长期潜伏。例如部分漏洞仅在 20MB 特殊格式输入条件下才会触发，万亿次测试也未必能够命中。
本次研究将程序测试入口转化为数学命题，证明在限定条件（小于 64MiB 任意输入）下，程序不会发生崩溃、内存越界等错误，覆盖全部执行路径。一旦证明过程受阻，就意味着程序存在潜在 Bug；Claude 可自动完成补丁修复，再继续开展后续证明工作。
实验中，研究人员在代码中预埋 7 个漏洞，随机测试漏掉 5 个，而形式化验证实现全部检出。在一款热门 PDF 阅读器中，Claude 一周发现漏洞数量，等同于以往一整年的安全报告产出量。
本次验证直接针对编译后真实运行的 RISC‑V 机器码，而非源代码。以cJSON 解析库为例，仅有 391 行 C 代码的解析入口，配套证明代码达到 63 万行，证明需要覆盖进程启动、内存分配器、运行时环境等整套底层逻辑，与业务直接相关的证明仅占十分之一。
项目整体尝试生成约 10 亿行证明，最终 1.8 亿行通过 Rocq 证明检查器校验，单份证明 CPU 核验耗时可达数十分钟至数小时。
形式化验证过去门槛极高，经典 seL4 微内核，编码仅耗费 2 人年，但全套形式化验证投入 20 人年，仅航空飞控这类高安全等级场景才会使用。
借助大模型，几周就完成上百个开源库的验证工作，并且 Claude 还自主构建 x86 指令集数学模型，复现 Ubuntu 用户态启动流程，同时找出 x86 官方文档数百处错误，捕获 CPU 硬件本身缺陷，实现从软件代码到芯片硬件的底层校验。
报告显示，大模型形式化验证能力迭代速度很快，验证速度大约每两个月翻番，证明片段还可跨项目复用，降低 token 消耗。研究团队以 Nix 软件生态测算：完成 OpenSSL 一次完整验证约 22 万美元，分摊到下游一万多个软件包，单个软件包成本仅 14 美元。
若保持当前迭代节奏，每年投入 1 亿美元，到 2027 年底，约 1.34 亿美元总投入，有望完成 Nix 生态 95% 机器码的形式化验证。对比全球每年数千亿美元网络安全相关损失，该技术拥有巨大现实价值。
近期网络安全事件频发，短时间内出现多起重大网络攻击，漏洞挖掘与攻击手段不断升级，人工打补丁已经难以跟上漏洞出现速度。目前该项目首批 25 个开源库、60 个入口的证明文件已开源至 GitHub，可供公众复现核验。
研究人员表示，大模型驱动的形式化验证，有望为互联网关键基础设施提供数学层面的安全兜底方案。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
