Lean이 이 프로그램을 올바르다고 증명했지만, 결국 버그를 찾았다

Claude 에이전트로 lean-zip을 fuzzing해, 검증된 Lean 구현에서도 실제 결함이 드러나는지 확인했다.

대상은 정리된 버전의 lean-zip 코드베이스였다. 정리 과정에서 theorem, specification, 문서, 그리고 C FFI로 연결된 zlib 구현을 제거하고, Lean으로 작성된 DEFLATE, gzip, ZIP, tar 관련 핵심 코드만 남겼다.

19시간 동안 16개의 병렬 fuzzer를 돌려 105,823,818회 실행했고, 그 결과:

• 애플리케이션 코드에서는 메모리 취약점이 발견되지 않았다.
• Lean 4 runtime의 lean_alloc_sarray에서 heap buffer overflow가 발견됐다.
• 검증되지 않은 archive parser에서는 denial-of-service가 확인됐다.

가장 중요한 취약점은 Lean runtime의 lean_alloc_sarray였다. ByteArray 같은 scalar array를 할당할 때 capacity 계산이 overflow를 일으켜, 실제로는 약 23바이트 수준의 작은 버퍼를 할당한 뒤 SIZE_MAX 크기의 읽기가 이어질 수 있었다. IO.FS.Handle.read를 통해 h.read n에 n = SIZE_MAX를 넣는 최소 재현 코드도 제시됐다. 이 문제는 Lean 4의 모든 버전에 영향을 주며, 패치 PR이 올라간 상태다.

두 번째 문제는 Archive.lean의 ZIP 파서였다. 중앙 디렉터리의 compressedSize 값을 검증 없이 h.read에 넘겨, 아주 작은 ZIP 파일도 비정상적으로 큰 크기를 선언하면 out of memory panic으로 이어졌다. 시스템 unzip은 파일 크기와 헤더를 대조해 이런 상황을 막지만, lean-zip은 그렇지 못했다.

검증이 잡지 못한 이유도 분명했다.

• ZIP archive parser는 애초에 증명 대상이 아니었다.
• runtime의 버그는 proof의 바깥, 즉 trusted computing base에 있었다.

결론적으로, 검증된 Lean 코드 자체는 105M회 fuzzing에서도 매우 견고했고, 발견된 두 문제는 모두 증명의 범위를 벗어난 지점에 있었다. 검증은 강력하지만, 무엇을 명세하고 무엇을 신뢰할지까지 포함해야 완성된다.