CVE-2026-72711 — Lean 4 커널 건전성 버그: 추론 캐시 오염

불투명 선언 FVar 캐시 오염을 통해 공리 없이 0 = 1 증명하기.

필드	값
버그 보고서	leanprover/lean4#14484
수정	leanprover/lean4#14498
영향받는 버전	Lean 4 ≤ `v4.31.0` / 모든 이전 버전
수정된 버전	nightly 2026-07-23+, v4.32.1 및 v4.33.0으로 백포트됨
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-488 (잘못된 세션에 데이터 요소 노출), CWE-20 (부적절한 입력 검증)
CVE	CVE-2026-72711

취약점 요약

Lean 4 커널의 environment::add_opaque 경로는 선언 본문에 대해 check_no_metavar_no_fvar를 호출하지 않습니다 — 정의와 정리는 값을 타입 검사하기 전에 이 클로저 검사를 수행하는 것과 다릅니다.

악의적인 메타프로그램은 이 누락을 추론 캐시 오염을 통해 악용합니다:

프라이밍 — 조작된 타입 표현식(cachePrimingType)은 False와 정의상 동일한 닫힌 베타-리덱스입니다. 이를 타입 검사하는 동안, 커널은 임시 지역 선언 _kernel_fresh.2 : False를 생성하고 그 추론된 타입을 type_checker 인스턴스의 추론 캐시에 캐시합니다.
컨텍스트 무효화 — 지역 컨텍스트는 복원되지만(임시 변수가 제거됨), 추론 캐시는 동일한 type_checker 인스턴스에 남아 있습니다. 이제 캐시 항목은 오래된 상태입니다 — 더 이상 스코프 내의 어떤 것도 참조하지 않는 식별자를 매핑하고 있습니다.
악용 — 불투명 선언의 값은 오래된 식별자를 가리키는 Expr.fvar입니다. 캐시 조회는 FVar 분기가 지역 컨텍스트 멤버십을 확인하기 전에 발생하여, 바인딩되지 않은 변수를 감지하지 못한 채 False를 타입으로 반환합니다.

그 결과는 커널이 수용한 False 타입의 불투명 상수이며, 이로부터 0 = 1이 자명하게 따라옵니다.

익스플로잇:

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

사용법

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

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

[*] Running CachePoisonFalse.lean with --trust=0 ...
kernel accepted bad : False
'bad' does not depend on any axioms
'assumptionFreeFalse' does not depend on any axioms
'zero_eq_one' does not depend on any axioms

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Depends on: no axioms

    Bug class:  Inference cache poisoning (CWE-488)
    Root cause: missing check_no_metavar_no_fvar in add_opaque
    Bug report: https://github.com/leanprover/lean4/issues/14484
    Fix:        https://github.com/leanprover/lean4/pull/14498

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

영향

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

형식 검증된 소프트웨어: 컴파일러, 암호화 라이브러리, 스마트 컨트랙트, 항공전자, 자동차 — Lean 증명 위에 구축된 모든 안전성 사례는 영향을 받는 버전으로 구축된 경우 무효입니다.
증명 운반 코드: Lake 패키지의 악성 의존성이 다운스트림 코드가 사용하는 불건전한 선언을 조용히 도입할 수 있습니다.
독립 검사기: 보고자는 leanchecker --fresh 재생도 익스플로잇을 수용함을 확인했습니다. comparator 내보내기 형식은 FVar를 표현할 수 없으므로 해당 검증 경로는 영향을 받지 않습니다.
AI 생성 증명: Lean을 신뢰할 수 있는 백엔드로 사용하는 AlphaProof, DeepSeek-Prover, Kimina-Prover와 같은 시스템은 정리를 증명하는 대신 커널 버그를 악용하는 증명을 생성할 수 있습니다.

기술적 세부 사항

근본 원인

src/kernel/environment.cpp에서 add_opaque 함수는 opaque 값의 타입을 검사하지만 클로저 검사를 수행하지 않습니다:

environment environment::add_opaque(declaration const & d, bool check) const {
    scoped_diagnostics diag(*this, check);
    opaque_val const & v = d.to_opaque_val();
    if (check) {
        type_checker checker(*this, diag.get());
        check_constant_val(*this, v.to_constant_val(), checker);
        // ← MISSING: check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
        expr val_type = checker.check(v.get_value(), v.get_lparams());
        // ...
    }
}

add_definition과 add_theorem은 모두 타입 검사 전에 해당 값에 대해 check_no_metavar_no_fvar를 호출합니다. add_opaque에서의 누락이 진입점입니다.

캐시 포이즈닝 메커니즘

type_checker의 추론 캐시는 표현식을 추론된 타입에 매핑합니다. infer_type_core에서 캐시 조회는 다음과 같습니다:

auto it = m_infer_type_cache[binfo_idx(bi)].find(e);
if (it != m_infer_type_cache[binfo_idx(bi)].end())
    return it->second;

FVar 분기가 로컬 컨텍스트 멤버십을 검증하기 전에 실행됩니다:

case expr_kind::FVar: {
    optional<local_decl> d = m_lctx.find_local_decl(e);
    if (!d) throw_kernel_exception(...);
    return d->get_type();
}

공격자는 타입 표현식을 통해 캐시 채우기를 제어하여, 오래된 항목의 이름(_kernel_fresh.2)을 예측 가능하고 공격 대상으로 만들 수 있습니다.

#14576과의 비교

측면	#14484 (이 버그)	#14576
버그 분류	캐시 포이즈닝	프로젝션 검증을 통한 타입 혼동
진입점	`add_opaque`에 클로저 검사 누락	중첩 귀납적 팬텀 매개변수
관련 캐시	예 — 추론 캐시	예 — expr 해시 비교
leanchecker 영향	예	예
comparator 영향	아니오 (FVar로 표현 불가)	예

크레딧

버그 발견: Patrick Hulin (@phulin), GPT-5.6 Sol의 도움
커널 수정: Joachim Breitner (@nomeata), PR #14498
PoC 패키징: Jonathan Brossard (@endrazine)

lean-cve-poc-14484

인기