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

(kirancodes.me)

1P by GN⁺ 5시간전 | ★ favorite | 댓글 1개

형식 검증된 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)”라는 질문이 남음

참고 링크

▲

GN⁺ 5시간전 [-]

Hacker News 의견들

이 글의 제목과 프레이밍이 좀 이상하게 느껴졌음
실제로 저자는 증명된 코드 안에서는 버그나 오류를 찾지 못했다고 명시함
발견된 두 가지 버그는 증명 범위 밖에 있었고, 하나는 명세 누락, 다른 하나는 C++ 런타임의 힙 오버플로우였음
Lean의 런타임에서 버그가 발견된 것이지, 검증을 수행하는 커널이 아님을 강조하고 싶음
Lean 문서 링크 참고
- 검증된 시스템에서 버그를 논할 때는 전체 바이너리를 고려해야 한다고 생각함
  버퍼 오버플로우로 비트코인을 잃는다면, 그 버그가 런타임에 있었다는 사실은 위로가 되지 않음
  또, 프로그램이 크래시한다면 대부분의 사용자는 그것을 버그로 여길 것임
  Lean을 실제 프로덕션 환경에서 돌리는 사람들도 꽤 있을 것임
- 제목만 보고 Lean 커널에 버그가 있다고 생각했는데, 실제로는 Lean 런타임과 lean-zip에서 발견된 문제였음
  커널이 아니라면 증명 자체의 신뢰성에는 큰 영향이 없음
- lean-zip의 명세 누락은 검증 철학상 중요한 문제임
  “Hello world” 프로그램을 검증한다고 해도, 출력뿐 아니라 부수효과까지 명세해야 함
  런타임과 커널 사이의 경계에서 메모리 손상이 생긴다면, 증명의 신뢰도는 떨어질 수 있음
  결국 “무엇을 검증해야 하는가”를 명확히 정의하는 게 핵심임
- 이 사이트의 글 목록을 보니 점점 클릭베이트스러워지는 게 재미있었음
  관련 글 목록
- Lean 런타임의 버그를 lean-zip의 버그라고 하는 건, JRE의 버그를 Java 앱의 버그라고 하는 것과 같음
  저자가 의도적으로 오해를 유도한 것처럼 보임
나도 증명된 코드에서 비슷한 경험을 했음
내 경우는 오버플로우보다는 명세 결함(spec bug) 이 문제였음
명세가 잘못되면, 코드와 증명은 완벽해도 의도한 동작과 다르게 작동함
결국 검증의 어려움은 인간의 의도를 정확히 표현하는 데 있음
AI가 검증을 완벽히 해결할 거라는 믿음은 잘못된 확신을 줄 수 있음
- 나도 비슷한 경험이 있음
  Lean, TLA+, Z3 같은 도구로 증명 가능한 명세는 단순화되어 있고 많은 가정이 필요함
  그래도 이건 강력한 도구임
  복잡한 알고리즘의 버그를 좁혀서 명세 경계를 명확히 볼 수 있게 해줌
  AI 덕분에 이런 증명 작업이 훨씬 쉬워졌음
- 항상 드는 의문은 “검증 시스템 자체는 어떻게 신뢰할 수 있는가”임
  프로그램을 검증하는 또 다른 프로그램도 결국 버그가 있을 수 있음
  완전한 자기 검증은 불가능하다는 점에서 하이젠베르크의 불확정성 원리를 떠올리게 됨
  결국 검증은 “두 번째 독립적 구현”을 통해 신뢰도를 높이는 과정임
- 내 코드의 버그는 두 가지로 나뉨
  (1) 의도한 동작과 다르게 작동하는 경우
  (2) 의도한 대로 작동하지만 그 의도가 잘못된 경우
  증명 도우미는 (1)을 막아주지만 (2)는 막지 못함
  즉, 설계의 건전성은 증명할 수 없음
  seL4처럼 모든 걸 검증하는 건 너무 비싸고 오래 걸림
- 명세 자체를 검증할 방법이 필요하다고 생각함
  형식 논리 + 적대적 사고(adversarial thinking) 를 결합해, 프로그램이 할 일과 하지 말아야 할 일을 완전하게 나열하는 방식이 이상적임
제목이 클릭베이트처럼 느껴졌음
증명된 부분에는 버그가 없는데 왜 이렇게 썼는지 모르겠음
HN에서는 사실 기반의 글을 보고 싶은데, 이건 시간 낭비였음
- 검증된 소프트웨어에서 “증명을 위반하는 버그만 버그로 본다”는 게 공정한가?
  “버그 없음”이라 광고하지만, 실제로는 “명세가 완벽히 표현된 범위 내에서만”임
  완벽히 옳더라도 현실에서는 죽은 채로 옳을 수 있음 — 즉, 이론적으로는 맞지만 실제로는 망가질 수 있음
- 제목이 기술적으로는 맞지만, lean-zip의 비검증 코드에서 생긴 문제를 마치 증명된 부분의 버그처럼 표현함
- 결과적으로 “증명된 부분의 범위를 명확히 하라”는 메시지는 흥미롭고 타당함
- 두 번째 버그는 근거 없이 만들어낸 것처럼 보임
  코드 참조도 없고, 실제 코드를 보면 오해임을 알 수 있음
- 결국 lean-zip은 단순히 Zlib 바인딩일 뿐임
이 문제는 분산 시스템 검증에서도 자주 나타남
증명은 특정 조건(운영 범위) 안에서만 유효하고, 흥미로운 실패는 그 경계에서 발생함
TLA+도 마찬가지로, 현실이 가정에서 벗어나면 증명은 무의미해짐
내가 원하는 건 운영 범위를 기계적으로 명시하고, 런타임에서 이를 감시하는 기능임
- 나도 CPU의 하드웨어 버그를 직접 발견한 적이 있음
  하지만 대부분의 버그는 하드웨어가 아니라 사람이 문서를 안 읽어서 생김
  형식 모델링만으로도 버그 수를 엄청 줄일 수 있음
이건 예측 가능한 좋은 소식임
LLM이 형식 검증을 통과하는 코드를 만들 수 있다는 뜻임
앞으로는 버그가 점점 하드웨어 계층으로 이동할 것임
결국 하드웨어 명세의 형식화가 필요해질 것임
제조사가 이를 공개하지 않으면, 커뮤니티와의 갈등이 생길 수도 있음
장기적으로는 취약점의 멸종 혹은 의도적 삽입이라는 두 갈래로 나뉠 것임
처음엔 저자가 증명된 부분을 테스트하지 않았다고 생각했음
하지만 읽다 보니, 버그는 증명 범위 밖에서 발견된 것임
그래서 제목이 다소 과장된 표현으로 느껴졌음
- 글쓴이 본인이 직접 등장함
  검증된 시스템의 버그라면 전체 바이너리가 대상이 되어야 한다고 주장함
  실제로 Archive.lean의 압축 헤더 파싱 부분에서 크래시를 일으키는 입력을 발견했다고 밝힘
Donald Knuth의 유명한 말이 떠오름
“위 코드에 버그가 있을 수 있으니 주의하라. 나는 단지 그것이 옳다고 증명했을 뿐, 실행해보진 않았다”는 경고였음
파서를 검증하지 않은 것은 큰 실수로 보임
바이너리 포맷 파싱은 항상 위험한 영역임
핵심은 AI 에이전트가 fuzzer와 협업해 Lean에서 힙 버퍼 오버플로우를 발견했다는 점임
이건 꽤 큰 성과임
- 정말 유용한 발견이라고 생각함
Claude가 “이건 내가 분석한 코드 중 가장 메모리 안전한 코드베이스 중 하나”라고 말한 부분이 인상적이었음
하지만 이게 Claude가 처음 분석한 코드라는 농담처럼 들림
- RL로 광범위하게 훈련된 Claude가 처음 분석한 코드일 리 없음
  그가 이렇게 잘하는 이유가 바로 그 때문임
- 어쩌면 Claude는 우리가 모르는 뭔가를 비밀스럽게 하고 있는 것일지도 모름 😄

답변달기

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

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

퍼징 실험 개요

실험 환경

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

문제 원인

트리거 조건

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

문제 재현

형식 검증이 놓친 부분

DoS 취약점의 원인

런타임 오버플로우의 본질

검증된 코드의 안정성

105백만 회 실행 결과

Lean의 타입 시스템 효과

결론

핵심 교훈

참고 링크

함께 보면 좋은 글 β

Hacker News 의견들