Lean이 '이 프로그램은 안전하다'고 증명했는데, 런타임에서 버그가 나왔다

• 형식 검증 언어 Lean 4의 런타임 C 코드에서 힙 버퍼 오버플로우가 발견됨
  • 아이러니하게도 Lean은 "이 프로그램이 정확하다"를 수학적으로 증명하는 언어인데, 정작 자기 런타임이 고전적인 C 버그를 갖고 있었음
• 취약 함수: lean_alloc_sarray
  • ByteArray capacity n에 대해 할당 크기가 24 + n으로 계산됨
  • n이 SIZE_MAX(2^64 - 1)에 가까우면 24 + n이 정수 오버플로우로 랩어라운드 → 23바이트짜리 버퍼만 할당
  • 호출자는 그 버퍼에 SIZE_MAX 바이트를 읽어들임 → 힙 버퍼 오버플로우
• 트리거 방법
  • 156바이트짜리 조작된 ZIP 파일 하나면 충분함
  • ZIP64 compressedSize를 0xFFFFFFFFFFFFFFFF로 세팅
  • IO.FS.Handle.read가 내부적으로 lean_io_prim_handle_read → lean_alloc_sarray를 호출하면서 오버플로우 발생
• 5줄짜리 최소 재현 코드가 공개됨

  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) -- SIZE_MAX
    let _ ← h.read n -- lean_alloc_sarray에서 오버플로우

• lean_io_get_random_bytes에서도 동일한 패턴 존재함
• 영향 범위: Lean 4 전 버전, v4.31.0-nightly-2026-04-11까지
• 수정 PR이 제출된 상태임

• lean-zip에서도 별도의 DoS 취약점 발견
  • readExact 함수가 ZIP 헤더의 compressedSize를 검증 없이 h.read에 그대로 전달함
  • 수 엑사바이트를 주장하는 ZIP 파일을 열면 OOM 패닉 발생
  • 시스템 unzip은 헤더 크기를 실제 파일 크기와 대조하는데, lean-zip은 안 함

---

기술 맥락

• 왜 형식 검증 언어에서 이런 버그가 나올 수 있냐면, Lean 4의 증명이 커버하는 범위를 생각해 봐야 해요
  • Lean이 증명하는 건 순수 함수형 레이어에서의 정확성이에요. "이 함수는 이런 입력에 대해 이런 출력을 보장한다" 같은 명제를 수학적으로 증명하는 거죠
  • 그런데 실제 실행은 C로 작성된 런타임이 담당하거든요. lean_alloc_sarray 같은 메모리 할당 함수는 그 증명 범위 밖이에요
• 정수 오버플로우의 메커니즘을 좀 더 자세히 보면요
  • 64비트 시스템에서 size_t는 최대 2^64 - 1까지 표현해요
  • sizeof(lean_sarray_object)가 24바이트이고, 여기에 capacity를 더하는데요
  • capacity가 SIZE_MAX(= 2^64 - 1)이면 24 + (2^64 - 1) = 23이 돼요 (모듈러 연산)
  • 결과적으로 23바이트만 malloc하고, fread에는 SIZE_MAX를 넘기는 거예요
• ZIP64 포맷을 이용한 트리거가 영리한 게, ZIP64 확장 필드는 compressedSize를 64비트로 표현할 수 있어서 0xFFFFFFFFFFFFFFFF를 합법적인 ZIP 구조 안에 넣을 수 있거든요
  • 실제 파일은 156바이트밖에 안 되지만, 헤더가 "이 엔트리의 압축 크기는 18 엑사바이트"라고 주장하는 거예요
• 이 사례가 보안 커뮤니티에서 주목받는 이유는, 형식 검증의 한계를 구체적으로 보여주기 때문이에요
  • 증명은 모델 안에서만 유효하고, 모델 바깥의 구현(FFI, 런타임, OS 인터페이스)은 별도로 검증해야 한다는 교훈이에요