CVE-2026-72711
Lean 4 4.32.2 이전 버전 커널이 바인딩되지 않은 자유 변수가 있는 불투명 선언을 허용함
- 게시됨
- 2026. 8. 24.
- 업데이트됨
- 2026. 10. 26.
- CNA 할당 중
- VulnCheck
- 증거 관찰됨
- 2026. 10. 26.
기본 CVSS
nvd · CVSS 4.0
CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N/E:X/CR:X/IR:X/AR:X/MAV:X/MAC:X/MAT:X/MPR:X/MUI:X/MVC:X/MVI:X/MVA:X/MSC:X/MSI:X/MSA:X/S:X/AU:X/R:X/V:X/RE:X/U:X낮음 · 다음 30일
- 백분위수
- 7.1%
- 모델 날짜
- 2026. 10. 25.
EPSS는 통계적 추정치이지 확실성이나 영향의 척도가 아닙니다. 이를 CVSS, KEV 상태, 노출 및 환경과 결합하세요.
요약
Lean 4 커널은 opaque 선언의 본문이 닫혀 있는지 확인하지 않습니다. environment::add_opaque는 definition 및 theorem 경로에서 수행하는 check_no_metavar_no_fvar 호출을 생략하므로, 로컬 컨텍스트에 없는 자유 변수를 포함하는 값이 즉시 거부되지 않습니다. 메타프로그램은 먼저 커널이 False 타입의 임시 로컬을 생성하도록 하고 그 타입을 타입 검사기의 추론 캐시에 기록한 다음, 해당 캐시 항목이 동일한 타입 검사기 인스턴스에 남아 있는 상태에서 로컬 컨텍스트를 복원하고, 마지막으로 값이 이제 바인딩되지 않은 변수인 opaque 선언을 제출할 수 있습니다. 캐시 조회는 로컬 컨텍스트의 멤버십을 검사할 분기보다 먼저 응답하므로, 커널은 캐시된 타입을 추론하고 False 타입의 opaque 상수를 허용하며, 이로부터 어떤 명제든 따라 나옵니다. 이 선언은 sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, 외부 코드 또는 수정된 .olean 파일 없이 최대 커널 검사 수준에서 일반적인 검사 경로를 통해 수용되며, 결과에는 공리가 포함되지 않습니다. 누락된 닫힘 검사를 추가하여 4.32.2에서 수정되었습니다.
소스
CVE-2026-72711 — Lean 4 커널 건전성 버그: 추론 캐시 오염
책임 있는 사용
귀하가 소유하고 있거나 테스트할 권한이 있는 시스템에 대해서만 취약점 정보를 사용하십시오. Kitploit은 공개 연구 메타데이터에 연결되며 익스플로잇 코드나 악성 페이로드를 저장하지 않습니다.