Lean이 프로그램의 정확성을 증명했지만, 그 안에서 버그가 발견됨

Lean으로 형식 검증된 lean-zip의 zlib 구현체를 퍼징한 결과, 검증된 애플리케이션 코드 자체는 메모리 취약점이 없었지만, Lean 4 런타임과 검증되지 않은 아카이브 파서에서 문제가 드러났다.

• AI 퍼저 Claude와 AFL++, AddressSanitizer, UBSan, Valgrind 등을 동원해 16개의 병렬 퍼저로 6개 공격면을 집중적으로 테스트했다.
• 총 105,823,818회 실행, 359개 시드, 19시간 동안 4개의 크래시 입력과 1개의 메모리 취약점이 확인됐다.
• 핵심 발견은 두 가지였다.

1) Lean 런타임의 힙 버퍼 오버플로우

lean_alloc_sarray에서 sizeof(lean_sarray_object) + elem_size * capacity 계산이 정수 오버플로우를 일으킬 수 있었다. capacity가 SIZE_MAX에 근접하면 작은 버퍼가 할당되고, 이후 큰 크기의 읽기가 들어오면서 힙 오버플로우가 발생한다.

• IO.FS.Handle.read에 매우 큰 nbytes를 넘기면 트리거된다.
• ZIP64 헤더의 compressedSize가 0xFFFFFFFFFFFFFFFF인 156바이트 파일로 재현 가능했다.
• 이 문제는 모든 Lean 4 버전에 영향을 준다고 정리되며, 수정 PR도 이미 제안됐다.

2) Archive.lean의 Out-of-Memory 기반 DoS

아카이브 파서의 readExact가 ZIP 중앙 디렉터리의 compressedSize를 검증 없이 그대로 사용해 비정상적으로 큰 메모리 할당을 시도했다. 그 결과 INTERNAL PANIC: out of memory로 프로세스가 종료될 수 있었다.

• 156바이트짜리 ZIP이 수 엑사바이트 크기를 주장하는 식으로 재현된다.
• 시스템 unzip은 이런 헤더 값을 검증하지만, lean-zip의 해당 경로는 그렇지 않았다.

이 사례가 보여주는 핵심은 분명하다. 형식 검증은 검증된 범위 안에서는 매우 강력하지만, 명세 밖의 코드와 런타임 계층까지 자동으로 보장하지는 못한다. 압축·해제 알고리듬은 안전했지만, 검증되지 않은 파서와 신뢰 기반 컴퓨팅 베이스(TCB) 내부의 런타임 버그가 전체 시스템 신뢰성을 흔들 수 있었다.