CVE-2026-72703

Riepilogo

Il controllo del guard in Rocq Prover tratta un parametro di un fixpoint mutuo annidato come uniforme senza esaminare le chiamate tra i diversi corpi di quel fixpoint. find_uniform_parameters in kernel/inductive.ml ispeziona solo le chiamate auto-ricorsive, quindi quando nessun corpo chiama se stesso la funzione conclude che ogni parametro è uniforme. Un parametro che cresce attraverso una chiamata incrociata da un corpo a un altro conserva pertanto la specifica del subterm ereditata dal fixpoint che lo racchiude, e una chiamata ricorsiva protetta da quella specifica viene accettata sebbene l'argomento non sia strutturalmente più piccolo. Una definizione non terminante viene ammessa come strutturalmente decrescente, il che produce un termine il cui valore è uguale al proprio successore e quindi una prova di False, dalla quale segue qualsiasi proposizione. La prova non richiede assiomi, plugin o flag unsafe e Print Assumptions la riporta come chiusa rispetto al contesto globale. Introdotto in Coq 8.20 e corretto in Rocq 9.2.0.

Fonti

• rocq-cve-poc-21682PoC

  CVE-2026-72703 — Rocq Guard Checker accetta un fixpoint non terminante tramite chiamate incrociate non verificate