endrazine/rocq-cve-poc-21682CVE-2026-72703 — Rocq Guard Checker가 미검증 교차 호출을 통해 비종료 Fixpoint를 허용함
가드 검사기의 균일 매개변수 우회를 통해 무공리로 0 = 1을 증명함.
Rocq 커널의 가드 검사기(fixpoint 종료 검증기)는 중첩된 상호 fixpoint의 모든
매개변수를, fixpoint 본문 간의 호출을 검사하지 않은 채 균일한 것으로 간주한다.
kernel/inductive.ml의 find_uniform_parameters 함수는 자기 재귀 호출만
검사하며, 어떤 본문도 자기 자신을 호출하지 않을 때 모든 매개변수를 균일하다고
판정한다. 교차 호출을 통해 증가하는 매개변수는 잘못된 subterm 명세를 유지할 수
있게 되고, 인자가 구조적으로 더 작지 않음에도 재귀 호출이 허용된다.
이로 인해 False를 증명하는 비종료 정의가 허용되며, 여기서 0 = 1을 포함한
모든 명제가 도출된다.
이 증명에는 공리, tactic, 플러그인, unsafe 플래그가 필요하지 않다. Print Assumptions는 이를 전역 컨텍스트에 대해 닫혀 있다고 보고한다.
docker build -t rocq-cve-poc-21682 .
docker run --rm rocq-cve-poc-21682
취약한 버전(Rocq 8.20 – <9.2.0)에서는 출력이 공리 없이 0 = 1의 증명을
확인해 준다.
패치된 버전(Rocq ≥9.2.0)에서는 가드 검사기가 해당 fixpoint를 거부한다.
Rocq/Coq 커널 검증 증명에 의존하는 모든 시스템은 추가 완화 조치 없이 취약한 버전에서 실행될 경우 영향을 받을 수 있다:
.v 파일이 불건전한 선언을 도입할 수 있는 증명 운반 코드kernel/inductive.ml의 find_uniform_parameters는 상호 fixpoint의 각 본문
내에서 자기 재귀 호출만 검사한다. 어떤 본문도 자기 재귀 호출을 포함하지 않을
때(모든 호출이 본문 간 교차 호출일 때), 모든 매개변수가 균일한 것으로 표시된다.
교차 호출을 거치며 실제로 변하는 매개변수는 잘못된 subterm 명세를 유지하게 되어,
가드 검사기가 구조적으로 감소하지 않는 인자에 대한 재귀 호출을 허용하게 된다.
| 필드 | 값 |
|---|---|
| CVE | CVE-2026-72703 |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (High) |
| 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 — 6.8 (Medium) |
| CWE | CWE-670 — 항상 잘못된 제어 흐름 구현 |
| 제품 | 영향 받음 | 수정됨 |
|---|---|---|
| Rocq Prover | 8.20 – <9.2.0 | 9.2.0 |
.vo 파일에 대해 coqchk를 실행한다.| 버그 보고서 | rocq-prover/rocq#21682 |
| 수정 | rocq-prover/rocq#21684 |
| VulnCheck 권고 | vulncheck.com |
| 날짜 | 사건 |
|---|---|
| 2025 | 버그 보고됨 (rocq-prover/rocq#21682) |
| 2025 | Rocq 9.2.0에서 수정 병합됨 (PR #21684) |
| 2026-08-24 | VulnCheck에서 CVE-2026-72703 공개 |
| 2026-08-24 | Docker로 재현 가능한 PoC 공개 |