CVE-2020-37268 — Rocq/Coq Print Assumptions lässt unsichere Universe-Prüfung über Parameter Inline aus

Umgehung des Proof-Audits über Modul-Funktor-Inlining — seit 2020 ungefixt.

Zusammenfassung der Schwachstelle

Print Assumptions meldet nicht, dass eine Definition mit deaktivierter Universe-Prüfung erstellt wurde, wenn diese Definition den Aufrufer über Parameter Inline in einem Modultyp erreicht. Die Funktor-Anwendung inlinet den Body des Parameters und verwirft den Datensatz des Kontexts Unset Universe Checking, sodass die resultierende Konstante keinerlei Hinweis auf die unsichere Operation zeigt.

Ein Modul kann daher eine Universe-Inkonsistenz nutzen, um False zu beweisen, und Print Assumptions meldet den abhängigen Beweis als abgeschlossen unter dem globalen Kontext — keine Axiome, keine sichtbaren Unsafe-Flags.

coqchk lehnt die resultierende kompilierte .vo-Datei zwar ab, aber das In-Process-Assumption-Audit (Print Assumptions) erkennt das Problem nicht.

Verwendung

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

Auf einer anfälligen Version (Rocq 8.11 – 9.2.0 und alle Coq 8.x mit dem Modulsystem) bestätigt die Ausgabe den Beweis von 0 = 1, wobei Print Assumptions ihn als abgeschlossen meldet.

Auswirkung

Jeder Workflow, der sich auf Print Assumptions als einzige Integritätsprüfung verlässt, kann betroffen sein:

• Formal verifizierte Compiler (CompCert)
• Verifizierte OS-Kernel (CertiKOS)
• Separation-Logic-Frameworks (Iris)
• Mathematische Bibliotheken (MathComp)
• Proof-Carrying Code, bei dem eine bösartige .v-Datei in einer Abhängigkeit unsichere Deklarationen einführen könnte, die das Assumption-Auditing bestehen
• Verifizierte Smart Contracts (ConCert)
• Jedes Projekt, das nicht routinemäßig coqchk auf kompilierter Ausgabe ausführt

Ursache

Wenn ein Modultyp Parameter Inline deklariert, inlinet die Funktor-Anwendung den Body des Parameters in den aufrufenden Kontext. Dieses Inlining verwirft die Metadaten, die festhalten, dass die ursprüngliche Definition unter Unset Universe Checking erzeugt wurde. Der Universe-Graph akzeptiert daher inkonsistente Universe-Constraints aus dem inline eingefügten Body, und Print Assumptions sieht keine Spur des unsicheren Kontexts.

Der Bug ist seit 2020 offen (Coq-Issue #12155) und ist in der Datei dev/doc/critical-bugs.md des Projekts dokumentiert. Stand Rocq 9.2.0 wurde kein Fix gemergt.

Bewertung

Feld	Wert
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

Betroffene Versionen

Produkt	Betroffen	Behoben
Coq	8.11 – 8.20	Nicht behoben
Rocq Prover	8.20 – 9.2.0	Nicht behoben

Gegenmaßnahmen

• coqchk ausführen auf allen kompilierten .vo-Dateien, bevor Beweisen in der Produktion vertraut wird. coqchk erkennt die Universe-Inkonsistenz, die Print Assumptions übersieht.
• Modulabhängigkeiten prüfen — der Angriff erfordert einen Modultyp mit Parameter Inline, der unter Unset Universe Checking kompiliert wurde.
• Stand Rocq 9.2.0 ist keine gepatchte Version verfügbar.

Referenzen

Bug report	rocq-prover/rocq#12155
Critical bugs doc	dev/doc/critical-bugs.md
VulnCheck advisory	vulncheck.com

Zeitleiste

Datum	Ereignis
2020	Bug gemeldet von Jason Gross (coq/coq#12155)
2020–2026	Bug bleibt offen, dokumentiert in critical-bugs.md
2026-08-24	CVE-2020-37268 veröffentlicht von VulnCheck
2026-08-24	Docker-reproduzierbarer PoC veröffentlicht

Danksagung

• Bug-Entdeckung: Jason Gross
• PoC-Paketierung: Jonathan Brossard (@endrazine) — MOABI / PSIRT.com