Lean proved this program correct; then I found a bug
3 days ago
- #fuzzing
- #formal_verification
- #software_security
- 利用Lean形式化验证开发了一个称为lean-zip、经证明正确的zlib实现，旨在构建安全软件，以应对人工智能驱动漏洞发现能力不断增强的趋势。
- 通过使用AFL++和Claude AI等工具进行超过1.05亿次执行的模糊测试，未在已验证的应用代码中发现错误，但发现了Lean 4运行时的堆缓冲区溢出漏洞及lean-zip未经验证的归档解析器中的拒绝服务漏洞。
- 堆缓冲区溢出位于Lean运行时的lean_alloc_sarray函数中，影响所有Lean 4程序，由读取过大尺寸触发；修复方案尚在制定中，这凸显了验证依赖于底层运行时的正确性。
- 拒绝服务漏洞的成因是lean-zip未经形式化验证的归档解析器盲目信任ZIP头部的compressedSize字段，导致过度内存分配和程序崩溃。
- 验证能有效消除许多错误类别，如已验证代码的清洁测试结果所示，但其有效性受限于指定的属性及对基础运行时的信任，这强调了需要采取全面安全措施的重要性。