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

8 hours ago 3

형식 검증된 zlib 구현체를 퍼징한 결과, Lean 4 런타임의 lean_alloc_sarray에서 힙 버퍼 오버플로우가 발견됨
AI 퍼저 Claude와 AFL++, AddressSanitizer 등을 이용해 1억 회 이상 테스트한 끝에, 4개의 크래시와 1개의 메모리 취약점이 확인됨
발견된 문제는 런타임 오버플로우와 Archive.lean의 Out-of-Memory 기반 서비스 거부(DoS) 두 가지로 구분됨
검증된 압축·해제 알고리듬은 안전했지만, 검증되지 않은 아카이브 파서와 런타임 계층에서 취약점이 존재함
결과적으로 형식 검증은 강력하지만, 신뢰 기반 컴퓨팅 베이스(TCB) 의 안전성 확보 없이는 전체 시스템의 안정성을 보장할 수 없음

Lean 검증을 통과한 프로그램에서 발견된 버그

Lean으로 형식 검증된 zlib 구현체를 퍼징한 결과, Lean 4 런타임에서 힙 버퍼 오버플로우가 발견됨
- 검증된 애플리케이션 코드에는 메모리 취약점이 없었음
- 그러나 Lean 런타임의 lean_alloc_sarray 함수에서 오버플로우가 발생해 모든 Lean 4 버전에 영향을 미침
AI 기반 퍼저 Claude와 AFL++, AddressSanitizer, Valgrind, UBSan 등을 이용해 1억 회 이상의 퍼징을 수행
- lean-zip의 압축·해제·아카이브 처리 등 6개 공격면을 대상으로 16개의 병렬 퍼저를 구동
- 19시간 동안 4개의 크래시 입력과 1개의 메모리 취약점이 발견됨
두 가지 주요 버그가 확인됨
- Lean 런타임의 lean_alloc_sarray에서 힙 버퍼 오버플로우
- lean-zip의 Archive.lean 모듈에서 Out-of-Memory 기반 서비스 거부(DoS)
형식 검증의 한계가 드러남
- lean-zip의 압축·해제 알고리듬은 완전 검증되었으나, 아카이브 파서(Archive.lean)는 검증되지 않아 DoS 취약점이 존재
- 런타임 버그는 신뢰 기반 컴퓨팅 베이스(Trusted Computing Base) 내부 문제로, 모든 Lean 프로그램에 영향을 미침
결론적으로, Lean의 형식 검증은 애플리케이션 코드의 안정성을 입증했지만, 검증 범위 밖의 구성요소에서는 여전히 취약점이 존재함
- 검증은 적용된 범위 내에서만 강력하며, 기초 신뢰 계층의 안전성 확보가 필수적임

퍼징 실험 개요

대상 코드베이스는 lean-zip의 검증된 zlib 구현체
- 모든 정리(theorem)와 명세(specification), 문서, C FFI 바인딩을 제거해 순수 Lean 코드만 남김
- Claude가 코드가 검증된 사실을 인지하지 못하도록 하여 편향을 방지
실험 환경
- 16개의 병렬 퍼저가 ZIP, gzip, DEFLATE, tar, tar.gz, compression 등 6개 공격면을 대상으로 실행
- AddressSanitizer, UndefinedBehaviorSanitizer, Valgrind memcheck, cppcheck, flawfinder 등을 병행
- 48개의 수작업 익스플로잇 파일을 포함해 총 105,823,818회 실행, 359개의 시드 파일 사용
- 19시간 동안 4개의 크래시 입력과 1개의 메모리 취약점이 발견됨

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

취약 함수: lean_alloc_sarray
- 모든 ByteArray, FloatArray 등의 스칼라 배열을 할당하는 함수
- sizeof(lean_sarray_object) + elem_size * capacity 계산 시 정수 오버플로우 발생 가능
문제 원인
- capacity가 SIZE_MAX에 근접할 경우 덧셈이 오버플로우되어 작은 버퍼가 할당됨
- 이후 호출자가 n 바이트를 읽어들여 힙 버퍼 오버플로우 발생
트리거 조건
- lean_io_prim_handle_read에서 nbytes가 매우 큰 값일 때 발생
- ZIP64 헤더의 compressedSize가 0xFFFFFFFFFFFFFFFF인 156바이트 파일로 재현 가능
- Lean 4의 모든 버전(최신 nightly 포함)에 영향
- 재현 코드 예시
def main : IO Unit := do IO.FS.writeFile "test.bin" "hello" let h ← IO.FS.Handle.mk "test.bin" .read let n : USize := (0 : USize) - (1 : USize) let _ ← h.read n
- 위 코드 실행 시 lean_alloc_sarray에서 오버플로우 발생
- 수정 PR이 제출되어 있음

버그 2: lean-zip 아카이브 파서의 서비스 거부(DoS)

취약 함수: readExact (Archive.lean)
- ZIP 중앙 디렉터리의 compressedSize 필드를 검증 없이 그대로 사용
- h.read 호출 시 비정상적으로 큰 크기를 요청해 메모리 과다 할당 및 OOM 발생
문제 재현
- 156바이트 ZIP 파일이 수 엑사바이트(exabyte) 크기를 주장할 경우 INTERNAL PANIC: out of memory로 프로세스가 종료됨
- 시스템 unzip은 헤더 크기를 검증하지만, lean-zip은 이를 수행하지 않음

형식 검증이 놓친 부분

DoS 취약점의 원인
- Archive.lean 모듈은 검증되지 않은 영역
- 압축·해제 파이프라인(예: DEFLATE, Huffman, CRC32)은 완전 검증되어 문제 없음
- 검증이 적용되지 않은 부분에서 취약점 발생
런타임 오버플로우의 본질
- Lean 런타임은 신뢰 기반 컴퓨팅 베이스(TCB) 에 속함
- 모든 Lean 증명은 런타임의 정확성을 전제로 함
- 따라서 런타임 버그는 모든 Lean 프로그램의 안전성에 영향을 미침

검증된 코드의 안정성

105백만 회 실행 결과
- Lean이 생성한 C 코드에서 힙 오버플로우, use-after-free, 스택 오버플로우, UB, 배열 범위 초과 모두 없음
- Claude의 평가에 따르면 “가장 메모리 안전한 코드베이스 중 하나”로 분석됨
Lean의 타입 시스템 효과
- 의존 타입(dependent types) 과 well-founded 재귀 구조로 C/C++ 기반 zlib 구현에서 흔한 취약점(CVE 클래스)을 구조적으로 차단
결론
- 검증된 코드 영역은 매우 견고했으며 퍼저가 오류를 찾기 어려웠음
- 그러나 검증되지 않은 부분과 런타임 계층에서는 여전히 취약점 존재
- 검증은 적용된 범위와 신뢰 기반의 안전성에 의해 한정됨

핵심 교훈

형식 검증은 적용된 코드 영역 내에서는 매우 강력하지만, 검증되지 않은 주변 구성요소나 런타임 계층이 전체 안정성을 위협할 수 있음
신뢰 기반 컴퓨팅 베이스의 안전성 확보가 필수이며, 검증된 시스템이라도 “누가 감시자를 감시하는가(Quis custodiet ipsos custodes)”라는 질문이 남음