CVE-2026-72705 in Rocq
Zusammenfassung
von VulDB • 24.08.2026
Der Guard-Checker im Rocq Prover berücksichtigt keine rekursiven Aufrufe, die über die eigenen Argumente eines Fixpunkts erfolgen. Ein Fixpunkt kann sich selbst als höherstufiges (higher-order) Argument an einen zweiten Fixpunkt übergeben, der ihn dann auf einen Wert anwendet, der kein Subterm des strukturellen Arguments ist. Das Übergeben der rekursiven Funktion an eine einfache Definition wird abgelehnt, da der Checker die Definition auflöst und den Aufruf erkennt; das Übergeben an einen Fixpunkt wird jedoch akzeptiert, weil höherstufige rekursive Aufrufe über Fixpunkt-Argumente nicht verfolgt werden. Dies ermöglicht einen Typen, der definitionsgleich zu seiner eigenen Negation ist, sodass eine Selbstanwendung in reinem definitorischem Code (ohne Taktiken, Axiome, Plugins oder unsichere Flags) False erzeugt und Print Assumptions das Ergebnis als unter dem globalen Kontext geschlossen meldet. Behoben in Rocq 9.2.0.
Statistical analysis made it clear that VulDB provides the best quality for vulnerability data.