CVE-2026-72703 — Il guard checker di Rocq accetta un fixpoint non terminante tramite chiamate incrociate non verificate

Dimostrazione di 0 = 1 senza assiomi tramite il bypass dei parametri uniformi del guard checker.

Riepilogo della vulnerabilità

Il guard checker del kernel di Rocq (verificatore di terminazione dei fixpoint) considera tutti i parametri di un fixpoint mutuo annidato come uniformi senza esaminare le chiamate tra i corpi del fixpoint. La funzione find_uniform_parameters in kernel/inductive.ml ispeziona solo le chiamate auto-ricorsive; quando nessun corpo chiama sé stesso, ogni parametro viene giudicato uniforme. Un parametro che cresce attraverso una chiamata incrociata può quindi mantenere una specifica di subterm errata, e una chiamata ricorsiva viene accettata anche se il suo argomento non è strutturalmente più piccolo.

Ciò ammette una definizione non terminante che dimostra False, da cui segue qualsiasi proposizione — inclusa 0 = 1.

La dimostrazione non richiede assiomi, tattiche, plugin o flag non sicuri. Print Assumptions la riporta come chiusa rispetto al contesto globale.

Utilizzo

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

Su una versione vulnerabile (Rocq 8.20 – <9.2.0), l'output conferma la dimostrazione di 0 = 1 senza assiomi.

Su una versione corretta (Rocq ≥9.2.0), il guard checker rifiuta il fixpoint.

Impatto

Qualsiasi sistema che si affida a dimostrazioni verificate dal kernel di Rocq/Coq può essere interessato se eseguito su una versione vulnerabile senza mitigazioni aggiuntive:

• Compilatori formalmente verificati (CompCert)
• Kernel di sistemi operativi verificati (CertiKOS)
• Framework di logica di separazione (Iris)
• Librerie matematiche (MathComp)
• Proof-carrying code in cui un file .v malevolo in una dipendenza potrebbe introdurre dichiarazioni non corrette
• Smart contract verificati (ConCert)

Causa principale

find_uniform_parameters in kernel/inductive.ml ispeziona solo le chiamate auto-ricorsive all'interno di ciascun corpo di un fixpoint mutuo. Quando nessun corpo contiene una chiamata auto-ricorsiva (tutte le chiamate sono chiamate incrociate tra i corpi), ogni parametro viene marcato come uniforme. Un parametro che in realtà varia tra le chiamate incrociate mantiene una specifica di subterm errata, consentendo al guard checker di accettare una chiamata ricorsiva su un argomento non strutturalmente decrescente.

Punteggio

Campo	Valore
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 (Alto)
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 (Medio)
CWE	CWE-670 — Implementazione del flusso di controllo sempre errata

Versioni interessate

Prodotto	Interessate	Corrette
Rocq Prover	8.20 – <9.2.0	9.2.0

Mitigazione

• Aggiornare a Rocq 9.2.0 o successivo.
• Eseguire coqchk sui file .vo compilati come misura di difesa in profondità.

Riferimenti

Segnalazione del bug	rocq-prover/rocq#21682
Correzione	rocq-prover/rocq#21684
Avviso VulnCheck	vulncheck.com

Cronologia

Data	Evento
2025	Bug segnalato (rocq-prover/rocq#21682)
2025	Correzione unita (PR #21684) in Rocq 9.2.0
2026-08-24	CVE-2026-72703 pubblicato da VulnCheck
2026-08-24	PoC riproducibile con Docker pubblicato

Crediti

• Scoperta del bug: Tristan Stérin, Claude Opus 4.6 (Anthropic)
• Correzione del kernel: PR #21684
• Packaging del PoC: Jonathan Brossard (@endrazine) — MOABI / PSIRT.com