---
title: "Lean이 '이 프로그램은 안전하다'고 증명했는데, 런타임에서 버그가 나왔다"
published: 2026-04-14T00:25:08.000Z
canonical: https://jeff.news/article/1734
---
# Lean이 '이 프로그램은 안전하다'고 증명했는데, 런타임에서 버그가 나왔다

형식 검증 언어 Lean 4의 런타임에서 힙 버퍼 오버플로우가 발견됐다. lean_alloc_sarray 함수에서 정수 오버플로우가 발생해 156바이트짜리 조작된 ZIP 파일로 트리거 가능하며, lean-zip에서도 별도의 DoS 취약점이 확인됐다.

- 형식 검증 언어 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줄짜리 최소 재현 코드가 공개됨
  ```lean
  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이 제출된 상태임

> [!WARNING]
> 이 버그는 Lean 언어로 작성된 사용자 코드의 문제가 아님. Lean의 **런타임 자체**(C로 작성된 메모리 할당 레이어)에서 발생하는 정수 오버플로우임. 형식 검증이 커버하는 순수 함수형 레이어와는 별개의 영역이라 증명으로 잡을 수 없었음.

- 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 인터페이스)은 별도로 검증해야 한다는 교훈이에요

## 핵심 포인트

- lean_alloc_sarray에서 capacity가 SIZE_MAX에 가까우면 24+n이 정수 오버플로우 → 23바이트만 할당하고 SIZE_MAX 바이트를 읽음
- 156바이트 조작 ZIP 파일(ZIP64 compressedSize=0xFFFFFFFFFFFFFFFF)로 트리거 가능
- Lean 4 v4.31.0-nightly까지 모든 버전 영향
- lean-zip의 readExact도 compressedSize 미검증으로 OOM DoS 가능

## 인사이트

형식 검증이 증명하는 건 '명세 안에서의 정확성'이지, 런타임 C 코드의 안전성까지 보장하지 않는다는 것을 보여주는 사례다.