Cyber ·
CVE-2020-37268: Print Assumptions do Rocq/Coq pode omitir universos inseguros via Parameter Inline
Falha de solidez no sistema de módulos do Rocq/Coq permite que Print Assumptions declare fechada uma prova de False, sem axiomas ou sinalizadores inseguros visíveis. O título do aviso indica que não há correção desde 2020.
Este item do Radar é um aviso de segurança publicado em 26 de outubro de 2026 sobre o CVE-2020-37268, que afeta o sistema de módulos do Rocq, antes conhecido como Coq, um assistente de provas usado para verificação formal. Segundo o texto, quando um tipo de módulo declara Parameter Inline e a aplicação de um functor incorpora o corpo do parâmetro, os metadados que registram que a definição original foi produzida com Unset Universe Checking são descartados. Como resultado, o comando Print Assumptions pode relatar como fechada, no contexto global, uma prova de False sem axiomas ou sinalizadores inseguros visíveis. O título informa que o problema não tem correção desde 2020. A relevância está em equipes que dependem de provas formais para certificar software ou pesquisa: uma auditoria que parece limpa pode não ser confiável. A Rota Nacional não verifica provas em Rocq/Coq e não resolve esse problema de engenharia. Para conferir o aviso, consulte a versão original citada no bookmark, na lista de discussão oss-sec, e procure o identificador CVE-2020-37268 na base oficial de CVEs. Confira também as notas de versão do projeto Rocq. O texto do Radar é uma tradução automática, então prefira a fonte original em caso de dúvida.