CVE-2026-72703

Resumo

O verificador de guarda no Rocq Prover trata um parâmetro de um fixpoint mútuo aninhado como uniforme sem examinar as chamadas entre os diferentes corpos desse fixpoint. find_uniform_parameters em kernel/inductive.ml inspeciona apenas chamadas autorrecursivas, portanto, quando nenhum corpo chama a si mesmo, a função conclui que todo parâmetro é uniforme. Um parâmetro que cresce por meio de uma chamada cruzada de um corpo para outro mantém, assim, a especificação de subtermo herdada do fixpoint envolvente, e uma chamada recursiva protegida por essa especificação é aceita embora o argumento não seja estruturalmente menor. Uma definição não terminante é admitida como estruturalmente decrescente, o que produz um termo cujo valor é igual ao seu próprio sucessor e, portanto, uma prova de False, da qual qualquer proposição decorre. A prova não requer axiomas, plugins ou flags inseguras, e Print Assumptions a reporta como fechada sob o contexto global. Introduzido no Coq 8.20 e corrigido no Rocq 9.2.0.

Fontes

• rocq-cve-poc-21682PoC

  CVE-2026-72703 — O verificador Rocq Guard aceita ponto fixo não terminante por meio de chamadas cruzadas não verificadas