검증된 zlib 구현을 퍼징한 결과, Lean 런타임의 버퍼 오버플로와 검증 범위 밖의 서비스 거부 취약점을 발견한 이야기.
13 Apr, 2026 lean formal_verification security fuzzing
나는 검증된 zlib 구현을 퍼징했고, Lean 런타임에서 버퍼 오버플로를 발견했다.
AI 에이전트는 대규모 소프트웨어 시스템에서 취약점을 찾는 데 매우 뛰어나게 되고 있다.
Anthropic은 Mythos의 취약점 발견 능력에 꽤 겁을 먹었는지, 그것이 "너무 위험하다"며 공개하지 않기로 했다고 한다 (lol). 이런 최신 모델들에 대한 과장을 믿든 믿지 않든, 한 가지는 부정하기 어려워 보인다. 상황은 이미 명확하다.
보안 버그를 발견하는 비용은 급격히 무너지고 있으며, 오늘날 돌아가는 소프트웨어의 대다수는 그런 수준의 정밀한 검토를 견디도록 만들어진 적이 없다. 우리는 다가오는 소프트웨어 위기에 직면하고 있다.
이처럼 밀려오는 쓰나미 앞에서, 최근에는 형식 검증 을 해결책으로 보려는 관심이 점점 커지고 있다. 기계적 도구를 사용해 코드의 성질을 명시하고 증명한다면, 다가오는 공격의 공세를 버텨낼 수 있는 견고하고 안전하며 안정적인 소프트웨어를 만들 수 있을까?
Lean 생태계의 최근 한 발전은 이 질문을 향해 한 걸음 내디뎠다. 10개의 에이전트가 자율적으로 zlib 구현인 lean-zip을 구축하고 증명했는데, 이는 인상적인 이정표다. Lean FRO의 수석 설계자인 Leo De Moura의 말(여기)을 인용하자면 다음과 같다.
AI 슬롭에 대해서는 양해를 구하겠다 (보아하니 Leo는 그것을 꽤 좋아하는 듯하다). 핵심 결과는 lean-zip이 그저 또 하나의 zlib 구현이 아니라는 점이다. 이것은 처음부터 끝까지 올바르다고 검증된 구현이며, Lean이 구현 버그가 전혀 없음을 보장한다.
"올바르다고 검증되었다"는 것은 실제로 어떤 모습일까? 다음은 핵심 정리 중 하나다 (github).
theorem zlib_decompressSingle_compress (data : ByteArray) (level : UInt8)
(hsize : data.size < 1024 * 1024 * 1024) :
ZlibDecode.decompressSingle
(ZlibEncode.compress data level) = .ok data
1기가바이트보다 작은 어떤 바이트 배열에 대해서도, ZlibDecode.decompressSingle을 ZlibEncode.compress의 출력에 호출하면 원래 데이터가 나온다. 압축 해제 함수는 정확히 압축의 역함수다. 이 함수 쌍은 완전히 올바르다.
정말 그럴까?
나는 주말 동안 lean-zip에 Claude 에이전트를 붙였고, AFL++, AddressSanitizer, Valgrind, UBSan을 사용하게 했다. 1억 500만 회가 넘는 퍼징 실행 끝에, 다음을 찾아냈다.
lean_alloc_sarray)의 힙 버퍼 오버플로. (버그 리포트, 수정 예정)lean-zip 아카이브 파서의 서비스 거부 취약점.실험 설정은 아주 단순했다. 나는 lean-zip 코드베이스를 가져와 축소한 버전을 만들고 Claude를 여기에 붙였다.
구체적으로 설정 과정에서 다음을 했다. (1) 모든 정리와 명세를 제거했고, (2) 모든 마크다운 문서를 삭제했으며, (3) 대체 구현으로 제공되던 lean-zip의 zlib용 C FFI 바인딩을 제거했다. 남은 것은 순수하게 검증된 코드뿐이었다. 즉 DEFLATE, gzip, ZIP 아카이브 처리, tar에 대한 네이티브 Lean 정의만 남겼다. 여기서 발견되는 모든 버그는 검증된 코드의 오류에 해당하게 된다.
정리와 문서를 제거한 이유는, 코드가 실제로 검증되었다는 사실을 미리 드러내 Claude 에이전트에 편향을 주는 일을 피하기 위해서였다. 코드에 "버그가 없다"는 것을 알면 선제적으로 포기할 수도 있다고 생각했고, 아무 정보 없이 접근하게 하면 편견 없이 소프트웨어를 탐색할 수 있을 것이라 봤다.
CLI를 통해 lean 구현에 접근할 수 있게 한 뒤, 퍼징 실험용 서버를 띄우고 Claude를 연결해 마음껏 돌리게 했다.
하룻밤 동안, Claude는 라이브러리의 6개 공격 표면에 걸쳐 병렬 퍼저 16개를 실행했다. 대상은 ZIP 추출, gzip 압축 해제, 원시 DEFLATE inflate, tar 추출, tar.gz, 압축 기능이었다. AddressSanitizer와 UndefinedBehaviorSanitizer를 적용한 별도 바이너리를 만들고, Valgrind memcheck를 실행했으며, 정적 분석을 위해 cppcheck와 flawfinder를 사용했고, 알려진 zlib CVE 패턴을 겨냥한 손수 작성한 익스플로잇 파일 48개도 만들었다.
전체적으로 이는 105,823,818회의 퍼징 실행으로 이어졌다. 시드 파일은 359개였다. 퍼저 16개가 약 19시간 동안 돌아가며 크래시를 일으키는 입력 4개와 코드 내 메모리 취약점 1개를 발견했다.
가장 중대한 발견은 힙 버퍼 오버플로였다. 하지만 이는 lean-zip 코드 안이 아니라 Lean 런타임 자체에 있었다.
취약한 함수는 lean_alloc_sarray로, Lean 4의 모든 스칼라 배열(ByteArray, FloatArray 등)을 할당한다.
lean_obj_res lean_alloc_sarray(
unsigned elem_size, size_t size, size_t capacity
) {
lean_sarray_object * o =
(lean_sarray_object*)lean_alloc_object(
sizeof(lean_sarray_object) + elem_size * capacity
);
// ...
}
용량이 n인 ByteArray의 경우 할당 크기는 24 + n이다. n이 SIZE_MAX(64비트 시스템에서는 )에 가까우면 이 덧셈이 래핑되어 작은 값이 된다. 런타임은 약 23바이트 정도의 아주 작은 버퍼를 할당하지만, 호출자는 그 안으로 n바이트를 읽으려 한다.
이 오버플로는 IO.FS.Handle.read를 뒷받침하는 C 함수 lean_io_prim_handle_read를 통해 유발할 수 있다.
obj_res lean_io_prim_handle_read(
b_obj_arg h, usize nbytes
) {
FILE * fp = io_get_handle(h);
obj_res res =
lean_alloc_sarray(1, 0, nbytes); // 여기서 오버플로
// ...
usize n = std::fread(
lean_sarray_cptr(res), 1, nbytes, fp
);
// ^^^ 23-byte buffer ^^^ SIZE_MAX count
ZIP64 compressedSize가 0xFFFFFFFFFFFFFFFF인 156바이트짜리 조작된 ZIP 파일 하나면 이를 유발하기에 충분하다. 같은 패턴은 lean_io_get_random_bytes에도 존재한다. 이 버그는 최신 nightly(v4.31.0-nightly-2026-04-11)를 포함해 현재까지의 모든 Lean 4 버전에 영향을 준다. 최소 재현 코드는 단 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의 PR이 대기 중이다.
AFL은 또한 lean-zip 자체 코드에서 서비스 거부 취약점도 찾아냈다. Archive.lean의 readExact 함수는 ZIP 중앙 디렉터리의 compressedSize 필드를 실제 파일 크기와 대조해 검증하지 않고 그대로 h.read에 넘긴다.
def readExact (h : IO.FS.Handle) (n : Nat) ... := do
-- ...
while buf.size < n do
let remaining := n - buf.size
let chunk ← h.read remaining.toUSize
-- n은 ZIP 헤더에서 온다
-- ...
수 엑사바이트 크기의 compressedSize를 주장하는 156바이트짜리 ZIP은, h.read가 가용 메모리보다 더 큰 메모리를 할당하려 하면서 프로세스를 INTERNAL PANIC: out of memory로 패닉시키게 만든다. 이것은 분명한 버그다. 시스템 unzip은 할당 전에 헤더 크기를 파일과 대조해 우아하게 처리하지만, lean-zip은 그렇게 하지 않아 OOM으로 크래시한다.
OOM 서비스 거부는 설명이 간단하다. 아카이브 파서는 애초에 검증된 적이 없었다. lean-zip의 증명은 압축과 압축 해제 파이프라인(DEFLATE, Huffman, CRC32, 왕복 올바름)을 다루지만, ZIP 헤더를 읽고 파일을 추출하는 모듈인 Archive.lean에는 원래의 축소 전 코드베이스에서조차 정리가 하나도 없다. compressedSize 필드는 신뢰할 수 없는 헤더에서 읽어 오며, 검증 없이 바로 할당에 사용된다. 이 상황은 Yang et al.의 CSmith 작업 (PLDI 2011)을 떠올리게 한다. 그 연구에서는 CompCert의 검증된 최적화 패스에서는 버그가 전혀 없었지만, 검증되지 않은 프런트엔드에서는 버그를 발견했다. 검증은 적용된 곳에서만 작동한다. 아카이브 파서는 lean-zip에서 검증이 적용되지 않은 부분이었다.
힙 버퍼 오버플로는 더 근본적인 문제다. lean_alloc_sarray는 Lean 런타임에 있는 C++ 함수로, 신뢰할 수 있는 계산 기반 의 일부다. 모든 Lean 증명은 런타임이 올바르다고 가정한다. 여기의 버그는 lean-zip에만 영향을 주는 것이 아니다. ByteArray를 할당하는 모든 Lean 4 프로그램에 영향을 준다.
여기서 오히려 더 놀라운 것은 긍정적인 결과다. 1억 500만 회의 실행 동안 애플리케이션 코드 에서는(즉 런타임을 제외하면) 힙 버퍼 오버플로가 0건, use-after-free가 0건, 스택 버퍼 오버플로가 0건, 정의되지 않은 동작이 0건(UBSan clean), Lean이 생성한 C 코드에서 배열 경계 밖 읽기가 0건이었다. 코드베이스가 검증되었다는 사실을 모른 채 Claude가 내린 평가를 인용하자면 다음과 같다.
이것은 내가 분석한 코드베이스 중 진심으로 가장 메모리 안전한 축에 속한다. 종속 타입과 well-founded recursion을 갖춘 Lean 타입 시스템은 C/C++ zip 구현을 괴롭혀 온 온갖 종류의 버그를 통째로 제거했다. 수십 년 동안 zlib를 괴롭혀 온 CVE 부류는 이 코드베이스에서는 구조적으로 불가능하다.
발견된 두 버그는 모두 증명이 다루는 경계 바깥에 있었다. 서비스 거부는 빠진 명세의 문제였다. 힙 오버플로는 전체 증명 구조가 올바르다고 가정하는 C++ 런타임, 즉 더 깊은 신뢰 기반의 문제였다(그리고 이제 이를 다루는 PR이 있다).
전반적으로 검증은 놀랄 만큼 견고하고 엄밀한 코드베이스를 만들어 냈다. AFL과 Claude는 오류를 찾는 데 정말 큰 어려움을 겪었다. 하지만 결국 문제를 찾아내긴 했다. 검증의 강도는 결국 어떤 질문을 할 줄 아는지, 그리고 어떤 기반을 신뢰하기로 선택하는지에 달려 있다.
Quis custodiet ipsos custodes?