Lean proved this program correct; then I found a bug
7 hours ago
- #fuzzing
- #formal_verification
- #software_security
- Formal verification in Lean was used to create a proven correct implementation of zlib, called lean-zip, aiming to build secure software as AI-driven vulnerability discovery becomes more powerful.
- Fuzzing with tools like AFL++ and Claude AI over 105 million executions found no bugs in the verified application code, but uncovered a heap buffer overflow in the Lean 4 runtime and a denial-of-service in lean-zip's unverified archive parser.
- The heap buffer overflow is in the Lean runtime's lean_alloc_sarray function, affecting all Lean 4 programs, triggered by reading large sizes; a fix is pending, highlighting that verification relies on the correctness of the underlying runtime.
- The denial-of-service bug occurs because lean-zip's archive parser, which was not formally verified, blindly trusts a ZIP header's compressedSize field, leading to excessive memory allocation and a crash.
- Verification effectively eliminates many bug classes, as shown by the clean results for the proven code, but its strength is limited to the properties specified and the trust in the foundational runtime, emphasizing the need for comprehensive security approaches.