Jason Gross

**Nome do Software Vulnerável e Versões Afetadas** Coq (versões afetadas não especificadas) **Description** O Print Assumptions não reporta quando uma definição é produzida enquanto a verificação de universo está desativada, caso essa definição chegue ao chamador através de Parameter Inline em um tipo de módulo. Ao aplicar um functor, o corpo do parâmetro é inlined, e esse processo remove o registro de que o termo foi construído sob Unset Universe Checking, fazendo com que a constante resultante não apresente vestígios da operação insegura. Dessa forma, uma implementação de módulo pode provar False usando uma inconsistência de universo e expô-la através de um parâmetro inlined, enquanto o Print Assumptions reporta a prova dependente como fechada sob o contexto global. Como o Print Assumptions é a auditoria de processo utilizada para confirmar que um desenvolvimento não repousa em suposições inesperadas, uma dependência construída dessa forma passa na auditoria enquanto prova proposições arbitrárias. O verificador independente coqchk rejeita o arquivo compilado resultante. **Recommendations** No momento, não há informações sobre uma versão mais recente que contenha a correção para esta vulnerabilidade. Utilize o verificador independente coqchk para validar arquivos compilados.