CVE-2026-72703

Zusammenfassung

Der Guard-Checker in Rocq Prover behandelt einen Parameter eines verschachtelten gegenseitigen Fixpunkts als uniform, ohne die Aufrufe zwischen den verschiedenen Rümpfen dieses Fixpunkts zu prüfen. find_uniform_parameters in kernel/inductive.ml untersucht nur selbstrekursive Aufrufe, sodass die Funktion, wenn kein Rumpf sich selbst aufruft, zu dem Schluss kommt, dass jeder Parameter uniform ist. Ein Parameter, der durch einen Queraufruf von einem Rumpf zu einem anderen wächst, behält daher die Subterm-Spezifikation bei, die er vom umschließenden Fixpunkt geerbt hat, und ein durch diese Spezifikation geschützter rekursiver Aufruf wird akzeptiert, obwohl das Argument nicht strukturell kleiner ist. Eine nicht terminierende Definition wird als strukturell abnehmend zugelassen, was einen Term ergibt, dessen Wert gleich seinem eigenen Nachfolger ist, und damit einen Beweis von False, aus dem jede Aussage folgt. Der Beweis erfordert keine Axiome, Plugins oder unsicheren Flags, und Print Assumptions meldet ihn als abgeschlossen unter dem globalen Kontext. Eingeführt in Coq 8.20 und behoben in Rocq 9.2.0.

Quellen

• rocq-cve-poc-21682PoC

  CVE-2026-72703 — Rocq Guard Checker akzeptiert nicht-terminierende Fixpoints durch ungeprüfte Cross-Calls