作者使用模糊测试在已验证的zlib实现中发现了一个缓冲区溢出漏洞，指出AI在漏洞发现方面能力强大，导致软件安全面临危机。尽管形式化验证被视为解决方案，但即使经过验证的代码仍可能存在漏洞，凸显当前软件安全的脆弱性。

标题：Lean验证了这段程序的正确性，然后我发现了漏洞

作者通过模糊测试在已验证的zlib实现中发现了一个Lean运行时的缓冲区溢出漏洞。

随着AI代理在发现大型软件系统漏洞方面变得非常擅长，软件安全面临严峻挑战。Anthropic公司甚至因担心其AI模型Mythos的漏洞发现能力"过于危险"而决定不发布它。无论你是否相信这些最新模型的炒作，一个事实已经显而易见：

发现安全漏洞的成本正在急剧下降，而当今运行的大多数软件从未经受过这种级别的审查。我们正面临一场迫在眉睫的软件危机。

面对这场即将到来的"海啸"，形式化验证作为一种解决方案受到越来越多的关注。Lean生态系统最近取得了一项突破性进展：10个AI代理自主构建并验证了zlib的实现——lean-zip。这个实现不仅功能完整，而且通过Lean验证，理论上可以保证完全没有实现错误。

但事实真的如此吗？

作者使用Claude代理对lean-zip进行了为期一周的测试，配备了AFL++、AddressSanitizer、Valgrind和UBSan等工具。在1.058亿次模糊测试执行后，发现了以下问题：

1. Lean运行时堆缓冲区溢出：在lean_alloc_sarray函数中发现漏洞，影响所有版本的Lean 4（漏洞报告，修复PR）
2. 拒绝服务漏洞：在lean-zip的归档解析器中发现（这部分代码未经验证）

测试设置

作者简化了lean-zip代码库，移除了所有定理、规范文档和C FFI绑定，只保留经过验证的代码部分。为了避免AI代理因知道代码"没有错误"而提前放弃，作者特意隐藏了验证信息。

测试过程中，Claude代理启动了16个并行模糊测试器，针对库的6个攻击面进行测试，共执行了105,823,818次模糊测试，发现了4个导致崩溃的输入和1个内存漏洞。

漏洞详情

1. Lean运行时堆缓冲区溢出：

   • 漏洞位于lean_alloc_sarray函数，该函数负责分配Lean 4中的所有标量数组
   • 当处理接近SIZE_MAX的大小时，会出现整数溢出，导致分配过小的缓冲区
   • 可通过一个156字节的特制ZIP文件触发

2. 归档解析器拒绝服务漏洞：

   • 问题出在Archive.lean模块中，该模块从未经过验证
   • 直接使用ZIP头中的compressedSize而不验证实际文件大小，导致可能分配过多内存

为什么验证没发现这些漏洞

• 拒绝服务漏洞存在于未经验证的归档解析器部分
• 堆缓冲区溢出则位于Lean运行时（验证所依赖的信任计算基础中）

结论

尽管发现了这些问题，验证仍然取得了显著成效：在1亿多次执行中，应用代码本身（不包括运行时）没有发现任何内存安全问题。正如Claude对代码库的评价：

这确实是我分析过的最内存安全的代码库之一。Lean的类型系统消除了困扰C/C++ zip实现的整类错误。

形式化验证确实能产生非常健壮的代码，但它的有效性取决于你提出的问题和你选择信任的基础。正如古语所问：谁来监督监督者？

相关链接

• lean-zip项目
• Lean 4漏洞报告

以下是评论内容的总结：

1. 关于形式化验证的局限性

   • 主要观点：形式化验证只能确保代码符合规范，但规范本身可能有缺陷或未覆盖所有情况。
   • 论据：
     • "If you have a spec that isn’t correct, you can certainly write code that conforms to that spec and write proofs to support it."（porcoda）
     • "Formal proofs can only ever work to validate against requirements... But a major issue with a lot of modern software is that the requirements themselves can be incorrect."（jongjong）

2. 标题与内容的争议

   • 主要观点：文章标题具有误导性，因为被验证的代码部分并未发现错误。
   • 论据：
     • "The two bugs that were found both sat outside the boundary of what the proofs cover."（ctmnt）
     • "Clickbait title, the proved part of the program had no bugs?"（grg0）

3. 形式化验证的潜在价值

   • 主要观点：尽管存在局限性，形式化验证仍然是提高代码可靠性的重要工具。
   • 论据：
     • "I’m genuinely excited about AI agents and formal verification languages... it’s obviously the way forward."（sebstefan）
     • "Compression/decompression is a good problem for proof of correctness."（Animats）

4. 关于停机问题的哲学讨论

   • 主要观点：由于停机问题的存在，完全的程序正确性证明是不可能的。
   • 论据：
     • "Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible."（ernsheong）
     • "You can get asymptotically close to zero-bug proof, but you can never get there 100% of the way."（youknownothing）

5. AI与形式化验证的结合

   • 主要观点：AI工具（如模糊测试）可以帮助发现形式化验证未覆盖的问题。
   • 论据：
     • "They used an AI agent sending ideas to a fuzzer and discovered a heap buffer overflow in Lean. This is big."（vatsachak）
     • "The spec-completeness problem here is the same one that bites distributed systems verification."（ajaystream）