# Lean이 프로그램의 정확성을 증명했지만, 그 안에서 버그가 발견됨 > Clean Markdown view of GeekNews topic #28560. Use the original source for factual precision when an external source URL is present. ## Metadata - GeekNews HTML: [https://news.hada.io/topic?id=28560](https://news.hada.io/topic?id=28560) - GeekNews Markdown: [https://news.hada.io/topic/28560.md](https://news.hada.io/topic/28560.md) - Type: GN+ - Author: [neo](https://news.hada.io/@neo) - Published: 2026-04-16T01:32:53+09:00 - Updated: 2026-04-16T01:32:53+09:00 - Original source: [kirancodes.me](https://kirancodes.me/posts/log-who-watches-the-watchers.html) - Points: 1 - Comments: 1 ## Topic Body - **형식 검증된 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 포함)에 영향 - **재현 코드 예시** ```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) let _ ← h.read n ``` - 위 코드 실행 시 `lean_alloc_sarray`에서 오버플로우 발생 - [수정 PR](https://github.com/leanprover/lean4/pull/13392)이 제출되어 있음 - --- ### 버그 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)”라는 질문이 남음 --- ### 참고 링크 - [lean-zip on GitHub](https://github.com/kim-em/lean-zip) - [Lean 4 버그 리포트](https://github.com/leanprover/lean4/issues/13388) - [Lean 4 수정 PR #13392](https://github.com/leanprover/lean4/pull/13392) ## Comments ### Comment 55520 - Author: neo - Created: 2026-04-16T01:32:54+09:00 - Points: 1 ###### [Hacker News 의견들](https://news.ycombinator.com/item?id=47759709) - 이 글의 **제목과 프레이밍**이 좀 이상하게 느껴졌음 실제로 저자는 증명된 코드 안에서는 버그나 오류를 찾지 못했다고 명시함 발견된 두 가지 버그는 증명 범위 밖에 있었고, 하나는 **명세 누락**, 다른 하나는 **C++ 런타임의 힙 오버플로우**였음 Lean의 **런타임**에서 버그가 발견된 것이지, 검증을 수행하는 **커널**이 아님을 강조하고 싶음 [Lean 문서 링크](https://lean-lang.org/doc/reference/latest/Elaboration-and-C...) 참고 - 검증된 시스템에서 버그를 논할 때는 전체 **바이너리**를 고려해야 한다고 생각함 버퍼 오버플로우로 비트코인을 잃는다면, 그 버그가 런타임에 있었다는 사실은 위로가 되지 않음 또, 프로그램이 크래시한다면 대부분의 사용자는 그것을 버그로 여길 것임 Lean을 실제 프로덕션 환경에서 돌리는 사람들도 꽤 있을 것임 - 제목만 보고 Lean **커널**에 버그가 있다고 생각했는데, 실제로는 **Lean 런타임**과 lean-zip에서 발견된 문제였음 커널이 아니라면 증명 자체의 신뢰성에는 큰 영향이 없음 - lean-zip의 **명세 누락**은 검증 철학상 중요한 문제임 “Hello world” 프로그램을 검증한다고 해도, 출력뿐 아니라 **부수효과**까지 명세해야 함 런타임과 커널 사이의 경계에서 메모리 손상이 생긴다면, 증명의 신뢰도는 떨어질 수 있음 결국 “무엇을 검증해야 하는가”를 명확히 정의하는 게 핵심임 - 이 사이트의 글 목록을 보니 점점 **클릭베이트**스러워지는 게 재미있었음 [관련 글 목록](https://kirancodes.me/posts/log-who-watches-the-watchers.htm...) - 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는 우리가 모르는 뭔가를 **비밀스럽게 하고 있는 것**일지도 모름 😄