CVE-2026-72714 — 모듈 종료 후 Rocq 유니버스 검사 상태 동기화 해제

모듈 범위 유니버스 검사 플래그의 동기화 해제를 통해 공리 없이 0 = 1 증명하기.

필드	값
버그 리포트	rocq-prover/rocq#22287
수정	없음 (2026-08-16 기준 이슈 열려 있음)
영향받는 버전	Rocq ≤ 9.2.0 / Coq 8.x (stdlib에 Hurkens가 포함된 모든 버전)
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-72714

취약점 요약

Rocq Prover의 모듈 시스템은 Local Unset Universe Checking 플래그의 범위를 제대로 지정하지 못한다. 모듈 내부에서 사용될 때, 이 플래그는 모듈이 종료될 때 이전 상태로 복원되어야 한다. 그러나 유니버스 그래프(ugraph)는 플래그의 자체 복사본을 유지하며, 이는 모듈 종료 시 전역 상태와 동기화가 어긋나게 된다.

동기화가 해제된 후:

Test Universe Checking은 켜짐을 보고한다 (전역 플래그는 복원됨)
ugraph는 여전히 유니버스 검사가 꺼져 있다 (자체 복사본은 복원되지 않음)
따라서 커널은 유니버스와 일관되지 않는 항을 오류 없이 받아들인다

유니버스 검사가 사실상 비활성화되면 Hurkens의 역설이 적용된다: TypeNeqSmallType.paradox는 유니버스 제약이 강제되지 않을 때 u < v인 Type@{u}와 Type@{v}가 혼동될 수 있다는 사실을 악용하여 False의 직접적인 증명을 도출한다.

익스플로잇:

공리, 플러그인, 안전하지 않은 기능을 사용하지 않음
Print Assumptions는 "Closed under the global context"를 보고함
표준 라이브러리의 일부인 Stdlib.Logic.Hurkens만 필요로 함
6줄의 증명 코드로 구성됨

사용법

docker build -t rocq-cve-poc-22287 .
docker run --rm rocq-cve-poc-22287

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

[*] Compiling ZeroEqOne.v ...
Universe Checking is on.
bad is defined
Closed under the global context
zero_eq_one is defined
Closed under the global context

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Depends on: no axioms (closed under the global context)

    Bug class:  Universe checking state desync (CWE-488)
    Root cause: ugraph retains stale Local Unset Universe Checking flag
    Bug report: https://github.com/rocq-prover/rocq/issues/22287

영향

Rocq의 커널 검증 증명을 신뢰하는 모든 시스템이 영향을 받습니다:

형식 검증 소프트웨어: CompCert(검증된 C 컴파일러), CertiKOS (검증된 OS 커널), Iris(동시성 분리 논리 프레임워크), MathComp — Rocq 증명을 기반으로 구축된 모든 안전성 사례는 증명 환경에 이 플래그 불일치가 있었다면 무효입니다.
증명 운반 코드(proof-carrying code): 의존성에 포함된 악의적인 .v 파일이 다운스트림 증명이 의존하는 불건전한 선언을 조용히 도입할 수 있습니다.
스마트 컨트랙트: 검증된 스마트 컨트랙트 개발에 Rocq를 사용하는 프로젝트 (예: ConCert)는 보안 보장이 무효화될 수 있습니다.

기술적 세부 사항

근본 원인

커널의 유니버스 그래프(ugraph)는 Universe Checking 플래그의 자체 사본을 포함합니다. 모듈이 Local Unset Universe Checking을 사용하면, 플래그는 전역 상태와 ugraph 양쪽에서 수정됩니다. 모듈이 닫힐 때 전역 상태는 모듈의 저장된 상태에서 복원되지만, ugraph의 사본은 동기화되지 않아 유니버스 검사가 사실상 비활성화된 상태로 남습니다.

공격 흐름

┌─────────────────────────────────────────────────────┐
│ 1. Universes u v.  Constraint u < v.                │
│    → Declare universes with strict ordering          │
├─────────────────────────────────────────────────────┤
│ 2. Module Off.                                       │
│      Local Unset Universe Checking.                  │
│    End Off.                                          │
│    → ugraph flag stays OFF after module closes        │
├─────────────────────────────────────────────────────┤
│ 3. Test Universe Checking.  → reports "on" (LIE)     │
├─────────────────────────────────────────────────────┤
│ 4. eapply TypeNeqSmallType.paradox; reflexivity.     │
│    → Kernel accepts universe-inconsistent proof       │
│    → False proved with no axioms                     │
├─────────────────────────────────────────────────────┤
│ 5. zero_eq_one : 0 = 1                              │
│    → Derived via exfalso                             │
└─────────────────────────────────────────────────────┘

Lean 4 커널 버그와의 비교

측면	Rocq #22287 (이 버그)	Lean #14484	Lean #14576
증명 보조기	Rocq (Coq)	Lean 4	Lean 4
버그 분류	모듈 시스템의 상태 비동기화	추론 캐시 오염	프로젝션을 통한 타입 혼동
익스플로잇 복잡도	6줄	~20줄	~50줄
유니버스/타입 시스템	유니버스 검사 우회됨	불투명 FVar 허용됨	팬텀 매개변수 탈출
수정 상태	미해결	수정됨 (PR #14498)	수정됨 (PR #14577)

크레딧

버그 발견: Gaëtan Gilbert (@SkySkimmer)
PoC 패키징: Jonathan Brossard (@endrazine)

rocq-cve-poc-22287

인기