CVE-2020-37268 — Rocq/Coq Print Assumptions omette il controllo unsafe degli universi tramite Parameter Inline

Aggiramento dell'audit delle prove tramite inlining di funtori di modulo — non risolto dal 2020.

Riepilogo della vulnerabilità

Print Assumptions non segnala che una definizione è stata costruita con il controllo degli universi disabilitato quando tale definizione raggiunge il chiamante tramite Parameter Inline in un tipo di modulo. L'applicazione del funtore effettua l'inlining del corpo del parametro e scarta la registrazione del contesto Unset Universe Checking, per cui la costante risultante non mostra alcun segno dell'operazione unsafe.

Un modulo può quindi sfruttare un'incoerenza degli universi per dimostrare False, e Print Assumptions riporta la prova dipendente come chiusa sotto il contesto globale — nessun assioma, nessun flag unsafe visibile.

coqchk rifiuta effettivamente il file .vo compilato risultante, ma l'audit delle assunzioni in-process (Print Assumptions) non rileva il problema.

Utilizzo

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

Su una versione vulnerabile (Rocq 8.11 – 9.2.0, e tutte le Coq 8.x con il sistema di moduli), l'output conferma la prova di 0 = 1 con Print Assumptions che la riporta come chiusa.

Impatto

Qualsiasi flusso di lavoro che si affida a Print Assumptions come unico controllo di integrità può essere interessato:

• 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 che superano l'audit delle assunzioni
• Smart contract verificati (ConCert)
• Qualsiasi progetto che non esegua abitualmente coqchk sull'output compilato

Causa principale

Quando un tipo di modulo dichiara Parameter Inline, l'applicazione del funtore effettua l'inlining del corpo del parametro nel contesto chiamante. Questo inlining scarta i metadati che registrano che la definizione originale è stata prodotta sotto Unset Universe Checking. Il grafo degli universi accetta quindi vincoli di universo incoerenti provenienti dal corpo inlinato, e Print Assumptions non vede alcuna traccia del contesto unsafe.

Il bug è aperto dal 2020 (issue Coq #12155) ed è documentato nel file dev/doc/critical-bugs.md del progetto. Nessuna correzione è stata integrata a partire da Rocq 9.2.0.

Punteggio

Campo	Valore
CVE	CVE-2020-37268
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (High)
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 (Medium)
CWE	CWE-778 — Insufficient Logging

Versioni interessate

Prodotto	Interessate	Corrette
Coq	8.11 – 8.20	Non corrette
Rocq Prover	8.20 – 9.2.0	Non corrette

Mitigazione

• Eseguire coqchk su tutti i file .vo compilati prima di fidarsi delle prove in produzione. coqchk rileva l'incoerenza degli universi che Print Assumptions non vede.
• Verificare le dipendenze dei moduli — l'attacco richiede un tipo di modulo con Parameter Inline compilato sotto Unset Universe Checking.
• Nessuna versione corretta è disponibile a partire da Rocq 9.2.0.

Riferimenti

Segnalazione del bug	rocq-prover/rocq#12155
Documento sui bug critici	dev/doc/critical-bugs.md
Avviso VulnCheck	vulncheck.com

Cronologia

Data	Evento
2020	Bug segnalato da Jason Gross (coq/coq#12155)
2020–2026	Il bug rimane aperto, documentato in critical-bugs.md
2026-08-24	CVE-2020-37268 pubblicato da VulnCheck
2026-08-24	PoC riproducibile con Docker pubblicato

Crediti

• Scoperta del bug: Jason Gross
• Packaging del PoC: Jonathan Brossard (@endrazine) — MOABI / PSIRT.com