CVE-2026-72705
Rocq Prover vor 9.2.0 Guard Checker akzeptiert Fixpoint als Argument höherer Ordnung
- 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
- 25.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 verfolgt keine rekursiven Aufrufe, die über die eigenen Argumente eines Fixpunkts erfolgen. Ein Fixpunkt kann sich selbst als Argument höherer Ordnung an einen zweiten Fixpunkt übergeben, der es dann auf einen Wert anwendet, der kein Subterm des strukturellen Arguments ist. Das Übergeben der rekursiven Funktion an eine einfache Definition wird abgelehnt, weil der Checker die Definition entfaltet und den Aufruf erkennt, aber das Übergeben an einen Fixpunkt wird akzeptiert, weil rekursive Aufrufe höherer Ordnung über Fixpunkt-Argumente nicht verfolgt werden. Dies lässt einen Typ zu, der definitionell gleich seiner eigenen Negation ist, sodass Selbstanwendung in rein definitionellem Code False erzeugt, ohne Taktiken, Axiome, Plugins oder unsichere Flags, und Print Assumptions meldet das Ergebnis als abgeschlossen unter dem globalen Kontext. Behoben in Rocq 9.2.0.
Quellen
CVE-2026-72705 — Rocq Guard Checker akzeptiert als Argument höherer Ordnung übergebenen Fixpoint
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.