endrazine/rocq-cve-poc-21682CVE-2026-72703 — Rocq Guard Checker akzeptiert nicht-terminierende Fixpoints durch ungeprüfte Cross-Calls
Axiomfreier Beweis von 0 = 1 durch Umgehung der einheitlichen Parameter des Guard Checkers.
Der Guard Checker des Rocq-Kernels (der Verifizierer für die Terminierung von Fixpoints) behandelt alle Parameter eines verschachtelten gegenseitigen Fixpoints als einheitlich, ohne die Aufrufe zwischen den Rümpfen des Fixpoints zu prüfen. Die Funktion find_uniform_parameters in kernel/inductive.ml untersucht nur selbstrekursive Aufrufe; wenn kein Rumpf sich selbst aufruft, wird jeder Parameter als einheitlich eingestuft. Ein Parameter, der durch einen Cross-Call wächst, kann dann eine fehlerhafte Subterm-Spezifikation beibehalten, und ein rekursiver Aufruf wird akzeptiert, obwohl sein Argument nicht strukturell kleiner ist.
Dies ermöglicht eine nicht-terminierende Definition, die False beweist, woraus jede Aussage folgt — einschließlich 0 = 1.
Der Beweis erfordert keine Axiome, Taktiken, Plugins oder unsicheren Flags. Print Assumptions meldet ihn als abgeschlossen unter dem globalen Kontext.
docker build -t rocq-cve-poc-21682 .
docker run --rm rocq-cve-poc-21682
Auf einer anfälligen Version (Rocq 8.20 – <9.2.0) bestätigt die Ausgabe den Beweis von 0 = 1 ohne Axiome.
Auf einer gepatchten Version (Rocq ≥9.2.0) lehnt der Guard Checker den Fixpoint ab.
Jedes System, das auf kernel-geprüften Beweisen von Rocq/Coq beruht, kann betroffen sein, wenn es auf einer anfälligen Version ohne zusätzliche Gegenmaßnahmen läuft:
.v-Datei in einer Abhängigkeit unsichere Deklarationen einführen könntefind_uniform_parameters in kernel/inductive.ml untersucht nur selbstrekursive Aufrufe innerhalb jedes Rumpfes eines gegenseitigen Fixpoints. Wenn kein Rumpf einen selbstrekursiven Aufruf enthält (alle Aufrufe sind Cross-Calls zwischen den Rümpfen), wird jeder Parameter als einheitlich markiert. Ein Parameter, der tatsächlich über Cross-Calls variiert, behält eine fehlerhafte Subterm-Spezifikation, wodurch der Guard Checker einen rekursiven Aufruf mit einem nicht strukturell abnehmenden Argument akzeptiert.
| Feld | Wert |
|---|---|
| CVE | CVE-2026-72703 |
| 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-670 — Always-Incorrect Control Flow Implementation |
| Produkt | Betroffen | Behoben |
|---|---|---|
| Rocq Prover | 8.20 – <9.2.0 | 9.2.0 |
coqchk auf kompilierten .vo-Dateien als Defense-in-Depth-Maßnahme aus.| Fehlerbericht | rocq-prover/rocq#21682 |
| Fix | rocq-prover/rocq#21684 |
| VulnCheck-Advisory | vulncheck.com |
| Datum | Ereignis |
|---|---|
| 2025 | Fehler gemeldet (rocq-prover/rocq#21682) |
| 2025 | Fix gemergt (PR #21684) in Rocq 9.2.0 |
| 2026-08-24 | CVE-2026-72703 von VulnCheck veröffentlicht |
| 2026-08-24 | Docker-reproduzierbarer PoC veröffentlicht |