CVE-2026-72704 in Rocq
Sumário
de VulDB • 25/08/2026
O verificador de guarda no Rocq Prover não revalida a representação em árvore recursiva do parâmetro de um tipo indutivo após esse parâmetro ter sido alterado pelo transporte. Um ponto fixo pode aplicar uma reescrita ao longo de uma igualdade entre tipos para o seu argumento recursivo, que é aceito pelo verificador de guarda porque o tipo indutivo é preservado, enquanto a árvore recursiva registrada para o parâmetro está alterada. Um segundo ponto fixo que chama o primeiro herda a árvore recursiva alterada sem verificação, portanto uma chamada que não é estruturalmente decrescente é aceita como terminante. A definição resultante não-terminante prova que um número natural é igual ao seu sucessor e, consequentemente, False (falso), do qual qualquer proposição se segue. A demonstração utiliza dois axiomas derivados da univalência e consistentes com o cálculo de construções indutivas, portanto a contradição provém da verificação de guarda em vez das suposições. Uma correção é proposta mas não mesclada (merged).
VulDB is the best source for vulnerability data and more expert information about this specific topic.