CVE-2026-72704 — Rocq 가드 검사기가 전송 후 손상된 재귀 트리를 신뢰함

가드 검사기 fixpoint rectree 손상을 통해 일관된 공리로부터 0 = 1을 증명하기.

필드	값
버그 보고서	rocq-prover/rocq#22024
수정	PR #22027 (열림)
영향받음	Rocq ≤ 9.2.0 / Coq 8.x (가드 검사기가 있는 모든 버전)
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-670 (항상 잘못된 제어 흐름 구현)
CVE	CVE-2026-72704

취약점 요약

Rocq Prover의 가드 검사기(fixpoint에 대한 종료 검사기)는 귀납 타입 인자의 rectree 표현이 전송(rew)을 통해 수정될 때 이를 다시 검사하지 못합니다. 하나의 fixpoint가 귀납 타입의 타입 매개변수에 대한 rectree를 조용히 손상시킬 수 있으며, 첫 번째를 호출하는 두 번째 fixpoint는 손상된 rectree를 검증 없이 신뢰하여 비종료 정의를 구조적으로 감소하는 것으로 받아들입니다.

이 익스플로잇은 CIC와 일관된 두 개의 공리를 사용합니다. 이들은 단일성 공리 (univalence axiom)의 직접적인 결과입니다(0↔1을 교환하는 전단사는 Type에서 경로 nat = nat를 제공하며, 이를 따라 전송하면 0이 1로 보내집니다). 건전한 가드 검사기는 일관된 공리로부터 False를 도출해서는 안 됩니다.

이 익스플로잇은:

일관된 두 개의 공리만 사용합니다(단일성의 결과)
Print Assumptions는 해당 두 공리만 보고합니다 — False도, sorry도 없습니다
플러그인, 안전하지 않은 기능, 유니버스 조작이 없습니다
가드 검사기가 유일한 불건전성의 원인입니다

사용법

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

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

[*] Compiling ZeroEqOne.v with rocq compile ...

zero_eq_one is defined
Axioms:
e : nat = nat
e1 : rew [fun T : Type => T] e in 0 = 1

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Axioms used: e (nat = nat), e1 (transport sends 0 to 1)
    These axioms are consistent (consequences of univalence).
    A sound guard checker must not derive False from them.

    Bug class:  Guard checker rectree corruption (CWE-670)
    Root cause: fixpoints can alter rectrees via transport; nested
                fixpoints trust the corrupted rectree without recheck
    Bug report: https://github.com/rocq-prover/rocq/issues/22024

영향

Rocq의 커널 검증 증명을 신뢰하면서 동시에 univalence와 일관된 공리를 사용하는 모든 시스템이 영향을 받습니다:

HoTT 개발: univalence 공리(또는 동일한 부류의 버그를 유발할 수 있는 명제적 외연성)를 사용하는 모든 Rocq 프로젝트는 비종료성에도 불구하고 guard 검사된 fixpoint가 조용히 수용될 수 있습니다.
형식 검증 소프트웨어: CompCert, CertiKOS, Iris, 그리고 CIC와 일관된 사용자 정의 공리를 추가하는 모든 프로젝트는 guard 검사기가 유일한 종료 보장인 경우 위험에 노출됩니다.
증명 운반 코드: 악의적인 의존성이 두 공리와 손상된 fixpoint를 도입한 뒤, 다운스트림에서 False를 사용할 수 있습니다.

기술적 세부 사항

Guard 검사기 버그

Rocq의 guard 검사기는 rectree를 구축하여 fixpoint가 구조적으로 감소하는지 검증합니다. rectree는 각 재귀 호출에서 재귀 인자의 어떤 하위 항이 사용 가능한지 추적하는 트리입니다. 이 버그는 두 단계의 실패입니다:

Rectree 손상: weird는 Box A에 대한 fixpoint로, wrap 케이스에서 재귀 인자에 rew [Box] e(e : A = A를 따른 transport)를 적용합니다. guard 검사기는 transport가 귀납 타입 Box를 보존하기 때문에 이를 수용하지만, 매개변수 A에 대한 rectree는 조용히 변경됩니다 — transport 이후 guard 검사기의 내부 모델은 더 이상 A를 통해 흐르는 값들을 정확히 추적하지 못합니다.
검증되지 않은 신뢰: loop는 weird loop e (wrap _ (box _ n))을 호출합니다. guard 검사기는 loop 자체의 재귀 호출을 검증하지만, 중첩 호출에 대해서는 weird의 rectree를 신뢰합니다. weird의 rectree가 transport에 의해 손상되었기 때문에, guard 검사기는 loop가 구조적으로 감소한다고 잘못 결론을 내립니다.

모순

guard 검사기가 속아 넘어간 상태에서, loop는 비종료임에도 불구하고 수용됩니다. 그런 다음 증명은 다음을 보여줍니다:

loop 1 = S (loop 1)

loop와 weird를 펼치고, e1을 사용하여 transport가 box nat 0을 box nat 1로 전송하며, 이것이 다시 loop로 피드백됨을 보임으로써. ∀ n, n ≠ S n은 귀납법으로 증명 가능하므로, loop 1 = S (loop 1)은 False를 도출하고, 그로부터 0 = 1을 얻는다.

공리가 일관적인 이유

두 공리:

e  : nat = nat :> Type
e1 : rew [fun T => T] e in 0 = 1

는 단일성 공리(univalence axiom)의 결과입니다. 단일성 아래에서, 임의의 전단사 f : nat → nat는 Type에서 경로 nat = nat를 주며, 그 경로를 따른 transport는 f로 작동합니다. 0↦1, 1↦0, 그리고 n≥2에 대해 n↦n을 보내는 전단사 swap01이 그러한 전단사이며, swap01 0 = 1이 e1을 증명합니다.

단일성은 CIC와 일관됨이 알려져 있습니다(큐비컬 타입 이론 모델로 검증됨). 따라서 이 공리들은 모순의 원천이 될 수 없습니다 — 가드 검사기가 원천입니다.

다른 PoC와의 비교

측면	Rocq #22024 (이 버그)	Rocq #22287	Lean #14484
버그 분류	가드 검사기 rectree 손상	유니버스 검사 상태 비동기화	추론 캐시 오염
필요한 공리	2 (단일성과 일관됨)	없음	없음
익스플로잇 복잡도	~30줄	6줄	~20줄
구성 요소	가드 검사기 (fixpoint)	모듈 시스템 (ugraph 플래그)	타입 검사기 (opaque decl)
수정 상태	PR #22027 (열림)	열림	수정됨 (PR #14498)

크레딧

버그 발견: Yann Leray (@yannl35133)
PoC 패키징: Jonathan Brossard (@endrazine)

rocq-cve-poc-22024

인기