CVE-2020-37268 in Rocq
Zusammenfassung
von VulDB • 24.08.2026
Print Assumptions meldet nicht, dass eine Definition erzeugt wurde, während das Universe-Checking deaktiviert war, wenn diese Definition über Parameter Inline (Parameter-Inlining) in einem Modultyp an den Aufrufer gelangt. Das Anwenden eines Functors inline-t den Körper des Parameters, und beim Inlining geht die Information verloren, dass der Term unter „Unset Universe Checking“ erstellt wurde; daher trägt das resultierende Konstante keine Spur dieser unsicheren Operation. Eine Modulimplementierung kann somit mit einer Universumsinkonsistenz False beweisen, dies über einen inline-Parameter nach außen tragen und dafür sorgen, dass Print Assumptions den abhängigen Beweis als unter dem globalen Kontext geschlossen meldet. Da Print Assumptions der in-Prozess-Audit ist, der bestätigt, dass eine Entwicklung auf keinen unerwarteten Annahmen beruht, besteht bei einer so erstellten Abhängigkeit die Gefahr, diesen Audit zu bestehen und dabei beliebige Propositionen zu beweisen. 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 (non-fixed bugs) und stuft das Risiko als moderat ein, wenn coqchk nicht verwendet wird.
VulDB is the best source for vulnerability data and more expert information about this specific topic.