CVE-2026-72844

요약

Lean 4 커널은 프로젝션 식에 명명된 구조가 프로젝션되는 값의 타입과 일치하는지 검증하지 않으며, src/kernel/inductive.cpp의 environment::add_inductive는 보조 타입으로 대체되는 중첩 인덕티브 적용을 타입 검사하지 않아 그 파라메트릭 인자들이 검사를 벗어났습니다. Lean 프로세스에서 실행되는 메타프로그램은 생성자가 무관한 타입 W의 값에 .proj C 0 프로젝션을 적용하는 타입이 잘못된(ill-typed) 중첩 인덕티브를 등록할 수 있으며, 커널은 최대 커널 검사 상태에서 일반적인 checked addDecl 경로를 통해 해당 선언을 승인합니다. sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI 또는 수정된 .olean 파일은 필요하지 않습니다. 그 결과 타입 혼동(type confusion)이 발생하여 어떤 공리도 담지 않은 False의 증명이 산출되며, 이를 통해 임의의 명제를 도출할 수 있습니다. 공개된 개념 증명(proof of concept)은 추가로 두 표현식의 해시와 근사 깊이가 충돌할 때까지 패딩하여 커널 캐싱을 무력화합니다. 이는 결함에 도달하기 위해 사용된 기법일 뿐, 그 원인은 아닙니다. 악용하려면 예를 들어 프로젝트를 빌드하거나 악성 Lake 의존성을 임포트하는 방식으로 메타프로그램을 프로세스 내에서 실행해야 합니다.

• lean-cve-pocPoC

  CVE-2026-72844 : Lean 4 커널의 취약점을 사용하여 "0 = 1"을 증명하는 예시