CVE-2020-37268
Coq und Rocq Prover Print Assumptions lässt unsichere Universe-Prüfung aus, die durch Parameter Inline eingebettet wurde
- 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
Print Assumptions meldet nicht, dass eine Definition erzeugt wurde, während die Universe-Prüfung deaktiviert war, wenn diese Definition den Aufrufer über Parameter Inline in einem Modultyp erreicht. Das Anwenden eines Funktors inlinet den Rumpf des Parameters, und das Inlining verwirft den Datensatz, dass der Term unter Unset Universe Checking erzeugt wurde, sodass die resultierende Konstante keine Spur der unsicheren Operation trägt. Eine Modulimplementierung kann daher unter Ausnutzung einer Universe-Inkonsistenz False beweisen, dies über einen inlineten Parameter offenlegen und erreichen, dass Print Assumptions den abhängigen Beweis als abgeschlossen unter dem globalen Kontext meldet. Da Print Assumptions die prozessinterne Prüfung ist, mit der bestätigt wird, dass eine Entwicklung auf keinen unerwarteten Annahmen beruht, besteht eine so aufgebaute Abhängigkeit diese Prüfung, während sie beliebige Aussagen beweist. Der eigenständige Prüfer coqchk lehnt die resultierende kompilierte Datei jedoch ab. Das Projekt dokumentiert dies in dev/doc/critical-bugs.md unter den nicht behobenen Fehlern und stuft das Risiko als moderat ein, wenn coqchk nicht verwendet wird.
Quellen
CVE-2020-37268 — Rocq/Coq Print Assumptions lässt unsichere Universe-Prüfung über Parameter Inline aus
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.