CVE-2026-72703

Nome do Software Vulnerável e Versões Afetadas Coq versões 8.20 through 9.1.x

Description O verificador de guarda trata incorretamente um parâmetro de um fixpoint mútuo aninhado como uniforme porque a função find uniform parameters em kernel/inductive.ml inspeciona apenas chamadas autorrecursivas. Quando nenhum corpo chama a si mesmo, o sistema conclui que todos os parâmetros são uniformes. Consequentemente, um parâmetro que cresce através de uma chamada cruzada entre diferentes corpos mantém a especificação de subtermo herdada do fixpoint envolvente. Isso permite que uma chamada recursiva seja aceita mesmo que o argumento não seja estruturalmente menor, permitindo que uma definição não terminante seja admitida como estruturalmente decrescente. Isso pode levar a uma prova de False, permitindo que qualquer proposição seja provada sem a necessidade de axiomas, plugins ou flags inseguras.

Recommendations Atualizar para a versão 9.2.0 do Rocq.