CVE-2026-72704 — Il guard checker di Rocq si fida di un albero ricorsivo corrotto dopo il trasporto

Dimostrare 0 = 1 da assiomi coerenti tramite la corruzione del rectree del punto fisso del guard checker.

Campo	Valore
Bug report	rocq-prover/rocq#22024
Fix	PR #22027 (aperta)
Affected	Rocq ≤ 9.2.0 / Coq 8.x (tutte le versioni con guard checker)
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1
CWE	CWE-670 (Implementazione del flusso di controllo sempre errata)
CVE	CVE-2026-72704

Riepilogo della vulnerabilità

Il guard checker del Rocq Prover (verificatore di terminazione per i punti fissi) non ricontrolla la rappresentazione rectree degli argomenti di tipo induttivo quando questi vengono modificati tramite trasporto (rew). Un punto fisso può corrompere silenziosamente il rectree per un parametro di tipo di un induttivo, e un secondo punto fisso che chiama il primo si fiderà del rectree corrotto senza verifica, accettando una definizione non terminante come strutturalmente decrescente.

L'exploit utilizza due assiomi che sono coerenti con CIC — sono dirette conseguenze dell'assioma di univalenza (la biiezione che scambia 0↔1 fornisce un percorso nat = nat in Type lungo il quale il trasporto invia 0 a 1). Un guard checker corretto non deve derivare False da assiomi coerenti.

L'exploit:

• Utilizza solo due assiomi coerenti (conseguenze dell'univalenza)
• Print Assumptions riporta solo quei due assiomi — nessun False, nessun sorry
• Nessun plugin, funzionalità non sicure o manipolazione di universi
• Il guard checker è l'unica fonte di non-solidità

Utilizzo

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

Output atteso su una versione vulnerabile di 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

Impatto

Qualsiasi sistema che si affida alle prove verificate dal kernel di Rocq e utilizza assiomi coerenti con l'univalenza è interessato:

• Sviluppi HoTT: qualsiasi progetto Rocq che utilizzi l'assioma di univalenza (o l'estensionalità proposizionale, che potrebbe innescare la stessa classe di bug) potrebbe vedere i propri fixpoint verificati dal guard checker accettati silenziosamente nonostante la non terminazione.
• Software formalmente verificato: CompCert, CertiKOS, Iris e qualsiasi progetto che aggiunga assiomi personalizzati coerenti con CIC è a rischio se il guard checker è l'unica garanzia di terminazione.
• Proof-carrying code: una dipendenza malevola può introdurre i due assiomi e il fixpoint corrotto, per poi utilizzare False a valle.

Dettagli tecnici

Il bug del guard checker

Il guard checker di Rocq verifica che i fixpoint siano strutturalmente decrescenti costruendo un rectree — un albero che traccia quali sotto-termini dell'argomento ricorsivo sono disponibili a ogni chiamata ricorsiva. Il bug è un fallimento in due fasi:

1. Corruzione del rectree: weird è un fixpoint su Box A che applica rew [Box] e (trasporto lungo e : A = A) all'argomento ricorsivo nel caso wrap. Il guard checker lo accetta perché il trasporto preserva il tipo induttivo Box, ma il rectree per il parametro A viene silenziosamente alterato — dopo il trasporto, il modello interno del guard checker non traccia più accuratamente quali valori fluiscono attraverso A.

2. Fiducia non verificata: loop chiama weird loop e (wrap _ (box _ n)). Il guard checker verifica le chiamate ricorsive di loop stesso ma si fida del rectree di weird per la chiamata annidata. Poiché il rectree di weird è stato corrotto dal trasporto, il guard checker conclude erroneamente che loop è strutturalmente decrescente.

La contraddizione

Con il guard checker ingannato, loop viene accettato nonostante sia non terminante. La dimostrazione mostra quindi:

loop 1 = S (loop 1)

svolgendo loop e weird, e usando e1 per mostrare che il transport invia box nat 0 a box nat 1, che a sua volta rientra in loop. Poiché ∀ n, n ≠ S n è dimostrabile per induzione, loop 1 = S (loop 1) produce False, e da esso 0 = 1.

Perché gli assiomi sono consistenti

I due assiomi:

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

sono conseguenze dell'assioma di univalenza. Sotto univalenza, qualsiasi biiezione f : nat → nat dà un percorso nat = nat in Type, e il trasporto lungo quel percorso agisce come f. La biiezione swap01 che manda 0↦1, 1↦0, e n↦n per n≥2 è una tale biiezione, con swap01 0 = 1 che testimonia e1.

È noto che l'univalenza è coerente con CIC (validata da modelli di teoria dei tipi cubica). Pertanto questi assiomi non possono essere la fonte della contraddizione — lo è il guard checker.

Confronto con altri PoC

Aspetto	Rocq #22024 (questo bug)	Rocq #22287	Lean #14484
Classe di bug	Corruzione del rectree del guard checker	Desincronizzazione dello stato di controllo degli universi	Avvelenamento della cache di inferenza
Assiomi necessari	2 (coerenti con l'univalenza)	Nessuno	Nessuno
Complessità dell'exploit	~30 righe	6 righe	~20 righe
Componente	Guard checker (fixpoint)	Sistema dei moduli (flag ugraph)	Type checker (dichiarazione opaca)
Stato della correzione	PR #22027 (aperta)	Aperta	Corretto (PR #14498)

Crediti

• Scoperta del bug: Yann Leray (@yannl35133)
• Packaging del PoC: Jonathan Brossard (@endrazine)