CVE-2026-72705
Rocq Prover 9.2.0 이전 버전의 가드 검사기가 고차 인수로 전달된 fixpoint를 허용하는 취약점
- 게시됨
- 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 상태, 노출 및 환경과 결합하세요.
요약
Rocq Prover의 guard checker는 fixpoint 자체 인자를 통해 이루어지는 재귀 호출을 추적하지 않는다. 하나의 fixpoint가 자기 자신을 두 번째 fixpoint에 고차 인자로 전달할 수 있으며, 두 번째 fixpoint는 이를 구조적 인자의 하위 항이 아닌 값에 적용한다. 재귀 함수를 일반 정의에 전달하면 checker가 정의를 펼쳐 호출을 관찰하기 때문에 거부되지만, fixpoint에 전달하면 fixpoint 인자를 통한 고차 재귀 호출이 추적되지 않기 때문에 허용된다. 이로 인해 자기 자신의 부정과 정의상 동일한 타입이 허용되며, 따라서 자기 적용은 전술, 공리, 플러그인 또는 unsafe 플래그 없이 순수하게 정의적인 코드에서 False를 생성하고, Print Assumptions는 그 결과를 전역 컨텍스트에 대해 닫혀 있다고 보고한다. Rocq 9.2.0에서 수정되었다.
소스
CVE-2026-72705 — Rocq Guard Checker가 고차 인수로 전달된 Fixpoint를 허용함
책임 있는 사용
귀하가 소유하고 있거나 테스트할 권한이 있는 시스템에 대해서만 취약점 정보를 사용하십시오. Kitploit은 공개 연구 메타데이터에 연결되며 익스플로잇 코드나 악성 페이로드를 저장하지 않습니다.