CVE-2026-72844: Lean 4 커널 건전성 버그

중첩 귀납 프로젝션 검증 우회를 통해 0 = 1을 공리 없이 증명하기.

취약점 요약

Lean 4 커널은 프로젝션 식에서 명명된 구조체가 프로젝션 대상 값의 타입과 일치하는지 확인하지 않습니다. 또한 src/kernel/inductive.cpp의 environment::add_inductive는 보조 타입으로 대체되는 중첩 귀납적 응용을 타입 검사하지 않았기 때문에, 해당 매개변수 인자들이 검사를 우회했습니다.

Lean 프로세스에서 실행되는 메타프로그램은 생성자가 관련 없는 타입 W의 값에 .proj C 0 프로젝션을 적용하는 타입이 잘못된 중첩 귀납적 타입을 등록할 수 있습니다. 커널은 최대 커널 검사 설정에서 일반적인 검사된 addDecl 경로를 통해 해당 선언을 승인합니다. 그 결과 타입 혼동이 발생하여 공리가 없는 False의 증명이 생성되며, 이를 통해 0 = 1을 포함한 임의의 명제를 도출할 수 있습니다.

이 익스플로잇:

• 검사된 addDecl 커널 경로만 사용
• --trust=0 (최대 검사)로 실행
• #print axioms를 통해 공리 없음을 보고
• sorry, unsafeCast, debug.skipKernelTC, FFI 또는 .olean 변조를 사용하지 않음

사용법

docker build -t lean-cve-poc .
docker run --rm lean-cve-poc

취약한 Lean 버전에서의 예상 출력:

[*] Running ZeroEqOne.lean with --trust=0 ...
'bad' does not depend on any axioms
'boom' does not depend on any axioms
'zero_eq_one' does not depend on any axioms
zero_eq_one : 0 = 1

[!] VULNERABILITY CONFIRMED — CVE-2026-72844

    zero_eq_one : 0 = 1
    Depends on: no axioms

패치된 Lean 버전에서는 커널이 타입이 잘못된 귀납적 타입을 거부하며 스크립트는 해당 버전이 취약하지 않다고 보고합니다.

영향

Lean 커널이 검사한 증명을 진실의 근거로 신뢰하는 모든 시스템이 영향을 받습니다. 여기에는 다음이 포함됩니다:

• 정형 검증 소프트웨어: 컴파일러, 암호화 라이브러리, 스마트 계약, 항공 전자, 자동차 — 영향받는 버전으로 빌드된 Lean 증명 기반 안전성 케이스는 모두 유효하지 않습니다.
• 증명 전달 코드: Lake 패키지의 악의적인 종속성이 다운스트림 코드가 사용하는 비건전한 선언을 조용히 도입할 수 있습니다.
• 독립 검사기: 동일한 종류의 버그가 Nanoda 독립 타입 검사기도 우회하는 것으로 나타났습니다.

기술적 세부 사항

근본 원인은 커널이 중첩 귀납적 타입을 처리하는 방식에 있습니다. 중첩 발생 I Ds is를 제거할 때 커널은 매개변수 인자 Ds가 귀납적 타입의 선언된 매개변수와 일치하는지 확인해야 합니다. 취약한 코드는 Ds의 프로젝션 식(.proj)이 올바른 구조체 이름을 참조하는지 확인하지 못합니다 — w : W이고 W ≠ C인 경우에도 .proj C 0 w가 허용됩니다.

해시 충돌(커널은 정의적 동일성 검사에서 Expr.hash 비교를 사용함)과 결합하면, 공격자는 커널의 내부 타입 할당이 실제 용어 의미론과 일치하지 않는 선언을 등록할 수 있으며, 이로 인해 타입 혼동과 False의 증명이 발생합니다.

참고 자료

• NVD: CVE-2026-72844
• VulnCheck 권고
• oss-security 공개
• Lean 4 이슈 #14576
• 수정 PR #14577
• 수정 커밋

크레딧

• 버그 발견 및 최소 PoC: @kiranandcode
• 원본 CollatzLean 익스플로잇: @xrchz (Ramana Kumar)
• 커널 수정: Leonardo de Moura (PR #14577)
• CVE 접수 및 PoC 패키징: Jonathan Brossard (@endrazine)