CVE-2026-72714 — Stato del controllo degli universi di Rocq desincronizzato dopo la chiusura del modulo

Dimostrazione di 0 = 1 senza assiomi tramite la desincronizzazione del flag di controllo degli universi con ambito di modulo.

Campo	Valore
Bug report	rocq-prover/rocq#22287
Fix	Nessuno (issue aperta al 2026-08-16)
Affected	Rocq ≤ 9.2.0 / Coq 8.x (tutte le versioni con Hurkens nella stdlib)
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1
CWE	CWE-488 (Exposure of Data Element to Wrong Session), CWE-20 (Improper Input Validation)
CVE	CVE-2026-72714

Riepilogo della vulnerabilità

Il sistema di moduli di Rocq Prover non riesce a limitare correttamente l'ambito del flag Local Unset Universe Checking. Quando viene usato all'interno di un modulo, il flag dovrebbe essere ripristinato al suo stato precedente alla chiusura del modulo. Tuttavia, il grafo degli universi (ugraph) mantiene una propria copia del flag, che si desincronizza dallo stato globale alla chiusura del modulo.

Dopo la desincronizzazione:

• Test Universe Checking riporta on (il flag globale è stato ripristinato)
• L'ugraph ha ancora il controllo degli universi off (la sua copia non è stata ripristinata)
• Il kernel accetta quindi termini inconsistenti rispetto agli universi senza errore

Con il controllo degli universi di fatto disabilitato, si applica il paradosso di Hurkens: TypeNeqSmallType.paradox sfrutta il fatto che Type@{u} e Type@{v} con u < v possono essere confusi quando i vincoli sugli universi non sono applicati, producendo una dimostrazione diretta di False.

L'exploit:

• Non usa alcun assioma, plugin o funzionalità non sicura
• Print Assumptions riporta "Closed under the global context"
• Richiede solo Stdlib.Logic.Hurkens (parte della libreria standard)
• È composto da 6 righe di codice di dimostrazione

Utilizzo

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

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

Impatto

Qualsiasi sistema che si affida alle prove verificate dal kernel di Rocq è interessato:

• Software formalmente verificato: CompCert (compilatore C verificato), CertiKOS (kernel OS verificato), Iris (framework di logica di separazione concorrente), MathComp — qualsiasi caso di sicurezza costruito su una prova Rocq è invalido se l'ambiente di prova presentava questa desincronizzazione del flag.
• Proof-carrying code: un file .v malevolo in una dipendenza può introdurre silenziosamente dichiarazioni non solide su cui si basano le prove a valle.
• Smart contract: i progetti che utilizzano Rocq per lo sviluppo verificato di smart contract (ad es., ConCert) potrebbero vedere annullate le proprie garanzie di sicurezza.

Dettagli tecnici

Causa principale

Il grafo degli universi (ugraph) nel kernel contiene una propria copia del flag Universe Checking. Quando un modulo utilizza Local Unset Universe Checking, il flag viene modificato sia nello stato globale che nell'ugraph. Quando il modulo si chiude, lo stato globale viene ripristinato dallo stato salvato del modulo, ma la copia dell'ugraph non viene sincronizzata, lasciando il controllo degli universi di fatto disabilitato.

Flusso dell'attacco

┌─────────────────────────────────────────────────────┐
│ 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                             │
└─────────────────────────────────────────────────────┘

Confronto con i bug del kernel di Lean 4

Aspetto	Rocq #22287 (questo bug)	Lean #14484	Lean #14576
Assistente di dimostrazione	Rocq (Coq)	Lean 4	Lean 4
Classe di bug	Desincronizzazione dello stato nel sistema dei moduli	Avvelenamento della cache di inferenza	Confusione di tipi tramite proiezioni
Complessità dell'exploit	6 righe	~20 righe	~50 righe
Universo/sistema dei tipi	Controllo degli universi aggirato	FVar opaco accettato	Parametri fantasma sfuggono
Stato della correzione	Aperto	Corretto (PR #14498)	Corretto (PR #14577)

Crediti

• Scoperta del bug: Gaëtan Gilbert (@SkySkimmer)
• Packaging del PoC: Jonathan Brossard (@endrazine)