endrazine/rocq-cve-poc-21683CVE-2026-72705 — Rocq Guard Checker akzeptiert als Argument höherer Ordnung übergebenen Fixpoint
Beweis von 0 = 1 ohne Axiome über Russells Paradoxon durch Umgehung des Guard Checkers mittels Fixpoint.
Autonom entdeckt von Claude Opus 4.6 (Anthropic).
| Feld | Wert |
|---|---|
| Fehlerbericht | rocq-prover/rocq#21683 |
| Fix | PR #21684 |
| Betroffen | Rocq ≤ 9.1.0 / alle Coq-Versionen mit Guard Checker |
| Behoben in | 9.2.0 |
| 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-72705 |
Der Guard Checker akzeptiert Fixpoints, die sich selbst als Argumente höherer Ordnung an einen anderen Fixpoint übergeben, der sie dann auf Nicht-Teilausdrücken des strukturellen Arguments aufruft. Die Übergabe einer rekursiven Funktion an eine Definition (eine Nicht-Fixpoint-Konstante) wird korrekt abgelehnt — der Guard Checker entfaltet sie und erkennt den problematischen Aufruf. Die Übergabe an einen Fixpoint wird jedoch fälschlicherweise akzeptiert.
Dies erzeugt ein Paradoxon im Stil von Russell in 4 Zeilen:
Definition delta (x : russell 1) : False := x x.
Definition omega : False := delta delta.
wobei russell 1 per Definition gleich russell 1 -> False ist — ein Typ,
der seine eigene Negation ist. Selbstanwendung liefert direkt False.
Der Exploit:
Print Assumptions meldet "Closed under the global context"False besteht aus 4 Zeilen funktionalen CodesQed — rein definitionaldocker build -t rocq-cve-poc-21683 .
docker run --rm rocq-cve-poc-21683
Jedes System, das Rocqs kernel-geprüften Beweisen vertraut, ist betroffen:
iterate_to_neg f n seed :=
match n with
| 0 => f seed -> False (* negate after n steps *)
| S m => iterate_to_neg f m seed
end
russell n :=
match n with
| 0 => True
| S m => iterate_to_neg russell 1 (S m) (* passes ITSELF *)
end
Der Guard-Checker sollte russell ablehnen, weil es sich selbst als
Argument höherer Ordnung an iterate_to_neg übergibt, das es dann auf S m
aufruft (kein Subterm von n). Der Checker verfolgt jedoch nur direkte
rekursive Aufrufe, nicht Aufrufe über Fixpunkt-Argumente höherer Ordnung.
russell 1 = iterate_to_neg russell 1 1
= iterate_to_neg russell 0 1
= russell 1 -> False
Also russell 1 ≡ russell 1 -> False. Dies ist die klassische Russell-Menge:
die Menge aller Mengen, die sich nicht selbst enthalten. Selbstanwendung ergibt:
delta : russell 1 -> False (* russell 1 = russell 1 -> False *)
delta x := x x (* x : russell 1 = russell 1 -> False *)
omega : False
omega := delta delta (* delta : russell 1 -> False = russell 1 *)
Dieser Fehler wurde autonom von Claude Opus 4.6 während eines nächtlichen
Fuzzing-Laufs entdeckt, der von Tristan Stérin (@tcosmo) eingerichtet wurde, basierend auf Hinweisen von
Yannick Forster (@yforster) zum Guard-Checker. Die KI identifizierte das
Muster der Umgehung des Fixpunkts höherer Ordnung und konstruierte den minimalen
iterate_to_neg/russell-Exploit.
Siehe: Zulip-Thread