CVE-2020-37268

Resumo

Print Assumptions não relata que uma definição foi produzida enquanto a verificação de universos estava desativada quando essa definição chega ao chamador por meio de Parameter Inline em um module type. A aplicação de um functor faz a inlining do corpo do parâmetro, e a inlining descarta o registro de que o termo foi construído sob Unset Universe Checking, de modo que a constante resultante não carrega nenhum vestígio da operação insegura. Uma implementação de módulo pode, portanto, provar False usando uma inconsistência de universos, expô-la por meio de um parâmetro inlined e fazer com que Print Assumptions relate a prova dependente como fechada sob o contexto global. Como Print Assumptions é a auditoria in-process usada para confirmar que um desenvolvimento não se apoia em suposições inesperadas, uma dependência construída dessa forma passa nessa auditoria enquanto prova proposições arbitrárias. O verificador autônomo coqchk rejeita o arquivo compilado resultante. O projeto registra isso em dev/doc/critical-bugs.md na seção de bugs não corrigidos e classifica o risco como moderado quando coqchk não é usado.

Fontes

• rocq-cve-poc-12155PoC

  CVE-2020-37268 — Rocq/Coq Print Assumptions omite a verificação insegura de universos via Parameter Inline