Cyber ·
CVE-2026-72703: falha no verificador de guardas do Rocq permite provar 0 = 1
Aviso de segurança sobre o verificador de guardas do kernel Rocq, que aceita um ponto fixo não terminante por chamadas cruzadas não verificadas e permite provar False sem axiomas declarados.
Segundo o aviso publicado por Jonathan Brossard em 25 de outubro de 2026 na lista oss-sec, o verificador de guardas do kernel do Rocq, um assistente de provas, tem uma falha de solidez. Ela permite construir uma prova verificada de False e, por extensão, de qualquer proposição, incluindo 0 = 1, sem axiomas, táticas, plugins ou sinalizadores inseguros. O relatório afirma que Print Assumptions mostra a prova como fechada no contexto global, ou seja, essa verificação habitual não detecta o problema. A causa descrita é que o verificador trata todos os parâmetros de um ponto fixo mútuo aninhado como uniformes, sem examinar as chamadas cruzadas entre eles. O identificador atribuído é CVE-2026-72703. Para consultar o original, procure o identificador ou o título na lista oss-sec de 2026, no quarto trimestre, e confira a versão corrigida do Rocq indicada pelos mantenedores antes de confiar em provas formais já produzidas.