CVE-2026-72714
Rocq Prover bis 9.2.0: Universum-Prüfungszustand nach Modulschluss desynchronisiert
- 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 Rocq Prover stellt die Kopie des Universe-Checking-Flags im Universe-Graph nicht wieder her, wenn ein Modul geschlossen wird, das die Prüfung lokal deaktiviert hatte. Ein lokales Unset Universe Checking innerhalb eines Moduls soll erwartungsgemäß nur bis zum Ende des Moduls gelten, und das globale Flag wird wiederhergestellt, doch der Universe-Graph behält seine eigene Kopie, die deaktiviert bleibt. Die beiden Sichten widersprechen sich dann: Test Universe Checking meldet die Prüfung als aktiviert, während der Kernel weiterhin universum-inkonsistente Terme akzeptiert. Da die Beschränkung zwischen zwei Universen nicht mehr durchgesetzt wird, greift Hurkens' Paradoxon und liefert einen Beweis für False, aus dem jede Aussage folgt. Der Beweis verwendet keine Axiome, Plugins oder unsicheren Funktionen, sobald das Modul geschlossen ist, und Print Assumptions meldet ihn als closed under the global context, sodass weder die Annahmenprüfung noch die Flag-Abfrage den tatsächlichen Kernel-Zustand widerspiegelt. Es ist kein Fix verfügbar.
Quellen
CVE-2026-72714 — Rocq-Universum-Prüfungszustand nach Modulschluss desynchronisiert
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.