CVE-2026-72704 — Rocq Guard Checker vertraut nach Transport auf einen korrumpierten rekursiven Baum

Beweis von 0 = 1 aus konsistenten Axiomen mittels Korruption des Fixpunkt-Rectrees des Guard Checkers.

Feld	Wert
Fehlerbericht	rocq-prover/rocq#22024
Fix	PR #22027 (offen)
Betroffen	Rocq ≤ 9.2.0 / Coq 8.x (alle Versionen mit Guard Checker)
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-670 (Always-Incorrect Control Flow Implementation)
CVE	CVE-2026-72704

Zusammenfassung der Schwachstelle

Der Guard Checker des Rocq Prover (Terminierungsprüfer für Fixpunkte) versäumt es, die Rectree-Repräsentation von Argumenten induktiver Typen erneut zu prüfen, wenn diese durch Transport (rew) verändert werden. Ein Fixpunkt kann den Rectree für einen Typparameter eines induktiven Typs stillschweigend korrumpieren, und ein zweiter Fixpunkt, der den ersten aufruft, vertraut dem korrumpierten Rectree ohne Verifikation und akzeptiert eine nicht terminierende Definition als strukturell absteigend.

Der Exploit verwendet zwei Axiome, die mit CIC konsistent sind — sie sind direkte Konsequenzen des Univalenz-Axioms (die Bijektion, die 0↔1 vertauscht, liefert einen Pfad nat = nat in Type, entlang dessen der Transport 0 auf 1 abbildet). Ein korrekter Guard Checker darf aus konsistenten Axiomen nicht False ableiten.

Der Exploit:

Verwendet nur zwei konsistente Axiome (Konsequenzen der Univalenz)
Print Assumptions meldet nur diese beiden Axiome — kein False, kein sorry
Keine Plugins, unsicheren Features oder Universum-Manipulationen
Der Guard Checker ist die einzige Quelle der Unkorrektheit

Verwendung

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

Erwartete Ausgabe bei einer anfälligen Rocq-Version:

[*] Compiling ZeroEqOne.v with rocq compile ...

zero_eq_one is defined
Axioms:
e : nat = nat
e1 : rew [fun T : Type => T] e in 0 = 1

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Axioms used: e (nat = nat), e1 (transport sends 0 to 1)
    These axioms are consistent (consequences of univalence).
    A sound guard checker must not derive False from them.

    Bug class:  Guard checker rectree corruption (CWE-670)
    Root cause: fixpoints can alter rectrees via transport; nested
                fixpoints trust the corrupted rectree without recheck
    Bug report: https://github.com/rocq-prover/rocq/issues/22024

Auswirkung

Jedes System, das Rocqs kernel-geprüften Beweisen vertraut und Axiome verwendet, die mit Univalenz konsistent sind, ist betroffen:

HoTT-Entwicklungen: Jedes Rocq-Projekt, das das Univalenz-Axiom (oder propositionale Extensionalität, die dieselbe Fehlerklasse auslösen kann) verwendet, könnte seine guard-geprüften Fixpunkte trotz Nicht-Terminierung stillschweigend akzeptiert bekommen.
Formal verifizierte Software: CompCert, CertiKOS, Iris und jedes Projekt, das benutzerdefinierte, mit CIC konsistente Axiome hinzufügt, ist gefährdet, wenn der Guard-Checker die einzige Terminierungsgarantie ist.
Proof-Carrying Code: Eine bösartige Abhängigkeit kann die beiden Axiome und den korrumpierten Fixpunkt einführen und dann False downstream verwenden.

Technische Details

Der Guard-Checker-Fehler

Rocqs Guard-Checker überprüft, ob Fixpunkte strukturell abnehmend sind, indem er einen Rectree aufbaut — einen Baum, der verfolgt, welche Subterme des rekursiven Arguments bei jedem rekursiven Aufruf verfügbar sind. Der Fehler ist ein zweistufiges Versagen:

Rectree-Korruption: weird ist ein Fixpunkt auf Box A, der rew [Box] e (Transport entlang e : A = A) auf das rekursive Argument im wrap-Fall anwendet. Der Guard-Checker akzeptiert dies, weil der Transport den induktiven Typ Box erhält, aber der Rectree für den Parameter A wird stillschweigend verändert — nach dem Transport verfolgt das interne Modell des Guard-Checkers nicht mehr genau, welche Werte durch A fließen.
Ungeprüftes Vertrauen: loop ruft weird loop e (wrap _ (box _ n)) auf. Der Guard-Checker überprüft die eigenen rekursiven Aufrufe von loop, vertraut aber dem Rectree von weird für den verschachtelten Aufruf. Da der Rectree von weird durch den Transport korrumpiert wurde, kommt der Guard-Checker fälschlicherweise zu dem Schluss, dass loop strukturell abnehmend ist.

Der Widerspruch

Mit getäuschtem Guard-Checker wird loop trotz Nicht-Terminierung akzeptiert. Der Beweis zeigt dann:

loop 1 = S (loop 1)

durch Entfalten von loop und weird und unter Verwendung von e1, um zu zeigen, dass der Transport box nat 0 an box nat 1 sendet, was wiederum in loop zurückfließt. Da ∀ n, n ≠ S n durch Induktion beweisbar ist, ergibt loop 1 = S (loop 1) False, und daraus 0 = 1.

Warum die Axiome konsistent sind

Die beiden Axiome:

e  : nat = nat :> Type
e1 : rew [fun T => T] e in 0 = 1

sind Konsequenzen des Univalenz-Axioms. Unter Univalenz ergibt jede Bijektion f : nat → nat einen Pfad nat = nat in Type, und der Transport entlang dieses Pfades wirkt als f. Die Bijektion swap01, die 0↦1, 1↦0 und n↦n für n≥2 abbildet, ist eine solche Bijektion, wobei swap01 0 = 1 e1 bezeugt.

Es ist bekannt, dass Univalenz mit CIC konsistent ist (validiert durch Modelle der kubischen Typentheorie). Daher können diese Axiome nicht die Quelle des Widerspruchs sein — der Guard-Checker ist es.

Vergleich mit anderen PoCs

Aspekt	Rocq #22024 (dieser Bug)	Rocq #22287	Lean #14484
Fehlerklasse	Guard-Checker-Rectree-Korruption	Zustandsdesynchronisation der Universe-Prüfung	Vergiftung des Inferenz-Caches
Benötigte Axiome	2 (konsistent mit Univalenz)	Keine	Keine
Exploit-Komplexität	~30 Zeilen	6 Zeilen	~20 Zeilen
Komponente	Guard-Checker (Fixpoint)	Modulsystem (ugraph-Flag)	Type-Checker (opaque decl)
Fix-Status	PR #22027 (offen)	Offen	Behoben (PR #14498)

Danksagungen

Fehlerentdeckung: Yann Leray (@yannl35133)
PoC-Verpackung: Jonathan Brossard (@endrazine)

rocq-cve-poc-22024

Beliebteste