CVE-2026-72704
Rocq Prover bis 9.2.0 Guard Checker vertraut nach Transport auf beschädigten rekursiven Baum
- Veröffentlicht
- 24.08.2026
- Aktualisiert
- 26.10.2026
- CNA zuweisen
- VulnCheck
- Beweise beobachtet
- 26.10.2026
Primäres CVSS
nvd · CVSS 4.0
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/E:X/CR:X/IR:X/AR:X/MAV:X/MAC:X/MAT:X/MPR:X/MUI:X/MVC:X/MVI:X/MVA:X/MSC:X/MSI:X/MSA:X/S:X/AU:X/R:X/V:X/RE:X/U:XNiedrig · nächste 30 Tage
- Perzentil
- 7,1 %
- Modelldatum
- 27.10.2026
EPSS ist eine statistische Schätzung, keine Gewissheit oder ein Maß für die Auswirkung. Kombinieren Sie es mit CVSS, KEV-Status, Belichtung und Ihrer Umgebung.
Zusammenfassung
Der Guard-Checker in Rocq Prover prüft die rekursive Baumdarstellung eines Parameters eines induktiven Typs nicht erneut, nachdem dieser Parameter durch Transport verändert wurde. Ein Fixpoint kann eine Umschreibung entlang einer Gleichheit zwischen Typen auf sein rekursives Argument anwenden, was der Guard-Checker akzeptiert, weil der induktive Typ erhalten bleibt, während der für den Parameter aufgezeichnete rekursive Baum verändert wird. Ein zweiter Fixpoint, der den ersten aufruft, erbt den veränderten rekursiven Baum ohne Verifikation, sodass ein Aufruf, der nicht strukturell absteigend ist, als terminierend akzeptiert wird. Die daraus resultierende nicht terminierende Definition beweist, dass eine natürliche Zahl gleich ihrem eigenen Nachfolger und daher False ist, woraus jede Aussage folgt. Die Demonstration verwendet zwei Axiome, die aus der Univalenz folgen und mit dem Kalkül der induktiven Konstruktionen konsistent sind, sodass der Widerspruch aus der Guard-Prüfung und nicht aus den Annahmen stammt. Ein Fix wird vorgeschlagen, aber nicht zusammengeführt.
Quellen
CVE-2026-72704 — Rocq Guard Checker vertraut nach Transport auf einen beschädigten rekursiven Baum
Verantwortungsvoller Umgang
Verwenden Sie Schwachstelleninformationen nur auf Systemen, die Sie besitzen oder zu deren Testen Sie berechtigt sind. Kitploit verlinkt auf öffentliche Forschungsmetadaten und speichert keinen Exploit-Code oder bösartige Payloads.