CVE-2026-72714 — Rocq-Universum-Prüfungsstatus nach Modulschluss desynchronisiert

Axiomfreier Beweis von 0 = 1 über die Desynchronisierung des modulbezogenen Universe-Checking-Flags.

Feld	Wert
Fehlerbericht	rocq-prover/rocq#22287
Fix	Keiner (Issue offen mit Stand 2026-08-16)
Betroffen	Rocq ≤ 9.2.0 / Coq 8.x (alle Versionen mit Hurkens in der 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

Zusammenfassung der Schwachstelle

Das Modulsystem des Rocq Prover versäumt es, das Flag Local Unset Universe Checking ordnungsgemäß abzugrenzen. Bei Verwendung innerhalb eines Moduls sollte das Flag beim Schließen des Moduls auf seinen vorherigen Zustand zurückgesetzt werden. Der Universum-Graph (ugraph) führt jedoch seine eigene Kopie des Flags, die beim Modulschluss mit dem globalen Zustand aus dem Takt gerät.

Nach der Desynchronisierung:

• Test Universe Checking meldet an (das globale Flag wurde zurückgesetzt)
• Der ugraph hat die Universum-Prüfung weiterhin aus (seine Kopie wurde nicht zurückgesetzt)
• Der Kernel akzeptiert daher universum-inkonsistente Terme ohne Fehler

Mit effektiv deaktivierter Universum-Prüfung greift Hurkens' Paradoxon: TypeNeqSmallType.paradox nutzt aus, dass Type@{u} und Type@{v} mit u < v verwechselt werden können, wenn Universum-Constraints nicht durchgesetzt werden, und liefert einen direkten Beweis von False.

Der Exploit:

• Verwendet keine Axiome, Plugins oder unsicheren Funktionen
• Print Assumptions meldet „Closed under the global context“
• Benötigt nur Stdlib.Logic.Hurkens (Teil der Standardbibliothek)
• Besteht aus 6 Zeilen Beweiscode

Verwendung

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

Erwartete Ausgabe bei einer anfälligen Rocq-Version:

[*] 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

Auswirkung

Jedes System, das auf den kernel-geprüften Beweisen von Rocq vertraut, ist betroffen:

• Formal verifizierte Software: CompCert (verifizierter C-Compiler), CertiKOS (verifizierter OS-Kernel), Iris (Framework für nebenläufige Separationslogik), MathComp — jeder Sicherheitsnachweis, der auf einem Rocq-Beweis aufbaut, ist ungültig, wenn die Beweisumgebung von dieser Flag-Desynchronisierung betroffen war.
• Proof-Carrying Code: Eine bösartige .v-Datei in einer Abhängigkeit kann stillschweigend unsichere Deklarationen einführen, auf die nachgelagerte Beweise sich stützen.
• Smart Contracts: Projekte, die Rocq für die verifizierte Smart-Contract- Entwicklung nutzen (z. B. ConCert), könnten ihre Sicherheitsgarantien verlieren.

Technische Details

Ursache

Der Universum-Graph (ugraph) im Kernel enthält eine eigene Kopie des Flags Universe Checking. Wenn ein Modul Local Unset Universe Checking verwendet, wird das Flag sowohl im globalen Zustand als auch im ugraph geändert. Wenn das Modul geschlossen wird, wird der globale Zustand aus dem gespeicherten Zustand des Moduls wiederhergestellt, aber die Kopie im ugraph wird nicht synchronisiert, wodurch die Universum-Prüfung effektiv deaktiviert bleibt.

Angriffsablauf

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

Vergleich mit Lean-4-Kernel-Bugs

Aspekt	Rocq #22287 (dieser Bug)	Lean #14484	Lean #14576
Proof-Assistent	Rocq (Coq)	Lean 4	Lean 4
Bug-Klasse	Zustands-Desynchronisation im Modulsystem	Vergiftung des Inferenz-Caches	Typverwechslung durch Projektionen
Exploit-Komplexität	6 Zeilen	~20 Zeilen	~50 Zeilen
Universum-/Typsystem	Universumsprüfung umgangen	Opaque FVar akzeptiert	Phantom-Parameter entkommen
Fix-Status	Offen	Behoben (PR #14498)	Behoben (PR #14577)

Danksagungen

• Bug-Entdeckung: Gaëtan Gilbert (@SkySkimmer)
• PoC-Verpackung: Jonathan Brossard (@endrazine)