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

Contornando a auditoria de provas por meio da inlining de functores de módulo — sem correção desde 2020.

Resumo da Vulnerabilidade

Print Assumptions falha em relatar que uma definição foi construída com a verificação de universos desativada quando essa definição chega ao chamador por meio de Parameter Inline em um tipo de módulo. A aplicação de functor faz a inlining do corpo do parâmetro e descarta o registro do contexto Unset Universe Checking, de modo que a constante resultante não mostra nenhum sinal da operação insegura.

Um módulo pode, portanto, usar uma inconsistência de universos para provar False, e Print Assumptions relata a prova dependente como fechada sob o contexto global — sem axiomas, sem flags inseguras visíveis.

coqchk de fato rejeita o arquivo .vo compilado resultante, mas a auditoria de suposições em processo (Print Assumptions) não detecta o problema.

Uso

docker build -t rocq-cve-poc-12155 .
docker run --rm rocq-cve-poc-12155

Em uma versão vulnerável (Rocq 8.11 – 9.2.0, e todos os Coq 8.x com o sistema de módulos), a saída confirma a prova de 0 = 1 com Print Assumptions relatando-a como fechada.

Impacto

Qualquer fluxo de trabalho que dependa de Print Assumptions como única verificação de integridade pode ser afetado:

• Compiladores formalmente verificados (CompCert)
• Kernels de SO verificados (CertiKOS)
• Frameworks de lógica de separação (Iris)
• Bibliotecas matemáticas (MathComp)
• Código com prova embutida (proof-carrying code), onde um arquivo .v malicioso em uma dependência poderia introduzir declarações não sólidas que passam pela auditoria de suposições
• Contratos inteligentes verificados (ConCert)
• Qualquer projeto que não execute rotineiramente coqchk na saída compilada

Causa Raiz

Quando um tipo de módulo declara Parameter Inline, a aplicação de functor faz a inlining do corpo do parâmetro no contexto chamador. Essa inlining descarta os metadados que registram que a definição original foi produzida sob Unset Universe Checking. O grafo de universos, portanto, aceita restrições de universos inconsistentes provenientes do corpo inlined, e Print Assumptions não vê nenhum vestígio do contexto inseguro.

O bug está aberto desde 2020 (issue #12155 do Coq) e está documentado no arquivo dev/doc/critical-bugs.md do projeto. Nenhuma correção foi mesclada até o Rocq 9.2.0.

Pontuação

Campo	Valor
CVE	CVE-2020-37268
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (Alto)
CVSS 4.0	AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N — 6.8 (Médio)
CWE	CWE-778 — Registro Insuficiente

Versões Afetadas

Produto	Afetado	Corrigido
Coq	8.11 – 8.20	Sem correção
Rocq Prover	8.20 – 9.2.0	Sem correção

Mitigação

• Execute coqchk em todos os arquivos .vo compilados antes de confiar em provas em produção. coqchk detecta a inconsistência de universos que Print Assumptions deixa passar.
• Audite as dependências de módulos — o ataque exige um tipo de módulo com Parameter Inline que tenha sido compilado sob Unset Universe Checking.
• Nenhuma versão corrigida está disponível até o Rocq 9.2.0.

Referências

Relatório de bug	rocq-prover/rocq#12155
Documento de bugs críticos	dev/doc/critical-bugs.md
Aviso da VulnCheck	vulncheck.com

Cronologia

Data	Evento
2020	Bug relatado por Jason Gross (coq/coq#12155)
2020–2026	Bug permanece aberto, documentado em critical-bugs.md
2026-08-24	CVE-2020-37268 publicado pela VulnCheck
2026-08-24	PoC reproduzível via Docker publicado

Créditos

• Descoberta do bug: Jason Gross
• Empacotamento do PoC: Jonathan Brossard (@endrazine) — MOABI / PSIRT.com