形式化验证的边界与局限

来源: kirancodes.me | Hacker News: 381 points | ★★★★★ 精选

AI agents正在大规模发现软件漏洞。但形式化验证是否真的能保证代码安全? Lean验证的zlib实现给出了令人深思的答案。

背景: 令人兴奋的开始

Lean团队10个AI agents自主构建并证明了lean-zip，这是一个zlib的实现，Lean证明了其端到端的正确性:

theorem zlib_decompressSingle_compress (data : ByteArray) (level : UInt8)
 (hsize : data.size < 1024 * 1024 * 1024) :
 ZlibDecode.decompressSingle
 (ZlibEncode.compress data level) = .ok data

对于任何小于1GB的字节数组，解压缩是压缩的精确逆函数。听起来完美无缺?

实验: 用AI fuzzing验证"已验证"的代码

作者用Claude agent + AFL++ + AddressSanitizer + Valgrind + UBSan对lean-zip进行 fuzzing。105,823,818次执行后:

• 验证的Lean应用程序代码中: 零个内存漏洞
• Lean 4 runtime中发现1个heap buffer overflow
• lean-zip的archive parser中发现1个denial-of-service

Bug 1: Lean Runtime的Heap Buffer Overflow

漏洞在lean_alloc_sarray中，当capacity接近SIZE_MAX时:

lean_sarray_object * o =
 (lean_sarray_object*)lean_alloc_object(
 sizeof(lean_sarray_object) + elem_size * capacity
 );
// 当 elem_size * capacity 接近 SIZE_MAX 时，整数溢出!
// 分配23字节但读取SIZE_MAX字节

触发方法: 一个156字节的ZIP文件，ZIP64 compressedSize设为0xFFFFFFFFFFFFFFFF。

关键洞见: 这是Trusted Computing Base (TCB)的一部分——每个Lean证明都假设runtime正确，但runtime是C++代码，不在验证范围内。

Bug 2: Archive Parser的OOM

archive parser从未被验证:

def readExact (h : IO.FS.Handle) (n : Nat) := do
 let chunk ← h.read remaining.toUSize
 -- n来自ZIP header，没有验证!

一个声称compressedSize是数exabytes的ZIP��导致process panic: INTERNAL PANIC: out of memory。

为什么验证没有抓住这些bug

• Bug 1: 在TCB中——C++ runtime，不在Lean证明范围内
• Bug 2: 根本没有验证过Archive.lean模块

验证只在它被应用的地方有效。边界之外是盲区。

Claude的评估(不知道代码被验证过)

This is genuinely one of the most memory-safe codebases I've analyzed. The Lean type system with dependent types and well-founded recursion has eliminated entire classes of bugs that plague C/C++ zip implementations.

核心结论

形式化验证产生了显著健壮的代码库——AFL和Claude很难找到错误。但它们还是找到了。验证的强度取决于:

1. 你能想到要问什么问题
2. 你选择信任什么作为基础

Quis custodiet ipsos custodes?

谁来验证验证者?

这是形式化验证最深层的哲学问题。证明本身需要元理论，元理论需要信任。当我们用工具验证代码时，代码只是变得"对某些属性正确"。但那些属性是否充分? TCB是否真的可信?

这个case不是验证失败的案例，而是验证边界的精美展示。

← 返回目录