CVE-2026-72703 in Rocq
Zusammenfassung
von VulDB • 24.08.2026
Der Guard-Checker im Rocq Prover behandelt einen Parameter eines verschachtelten mutual fixpoint als uniform, ohne die Aufrufe zwischen den verschiedenen Körpern dieses Fixpunkts zu untersuchen. find_uniform_parameters in kernel/inductive.ml prüft nur selbst-rekursive Aufrufe; daher schließt es, dass jeder Parameter uniform ist, wenn kein Körper sich selbst aufruft. Ein Parameter, der durch einen Cross-Call von einem Körper zum anderen wächst, behält die Unterausdrucks-Spezifikation (subterm specification), die er vom umgebenden Fixpunkt geerbt hat, und ein rekursiver Aufruf, der durch diese Spezifikation geschützt ist, wird akzeptiert, obwohl das Argument nicht strukturell kleiner ist. Eine nicht-terminierende Definition wird als strukturell abnehmend (structurally decreasing) zugelassen, was zu einem Term führt, dessen Wert seinem eigenen Nachfolger entspricht, und somit zu einem Beweis von False, aus dem jede beliebige Proposition folgt. Der Beweis erfordert keine Axiome, Plugins oder unsicheren Flags; Print Assumptions meldet ihn als unter dem globalen Kontext geschlossen (closed under the global context). Eingeführt in Coq 8.20 und behoben in Rocq 9.2.0.
Statistical analysis made it clear that VulDB provides the best quality for vulnerability data.