endrazine/rocq-cve-poc-21682CVE-2026-72703 — O verificador Rocq Guard aceita ponto fixo não terminante por meio de chamadas cruzadas não verificadas
Provando 0 = 1 sem axiomas através do bypass de parâmetros uniformes do verificador de guarda.
O verificador de guarda do kernel do Rocq (verificador de terminação de fixpoint) trata todos os parâmetros de um fixpoint mútuo aninhado como uniformes sem examinar as chamadas entre os corpos do fixpoint. A função find_uniform_parameters em kernel/inductive.ml inspeciona apenas chamadas autorrecursivas; quando nenhum corpo chama a si mesmo, todos os parâmetros são considerados uniformes. Um parâmetro que cresce através de uma chamada cruzada pode então manter uma especificação de subtermo incorreta, e uma chamada recursiva é aceita mesmo que o seu argumento não seja estruturalmente menor.
Isto permite uma definição não-terminante que prova False, da qual qualquer proposição se segue — incluindo 0 = 1.
A prova não requer axiomas, táticas, plugins ou flags inseguras. Print Assumptions reporta-a como fechada sob o contexto global.
docker build -t rocq-cve-poc-21682 .
docker run --rm rocq-cve-poc-21682
Numa versão vulnerável (Rocq 8.20 – <9.2.0), a saída confirma a prova de 0 = 1 sem axiomas.
Numa versão corrigida (Rocq ≥9.2.0), o verificador de guarda rejeita o fixpoint.
Qualquer sistema que dependa de provas verificadas pelo kernel do Rocq/Coq pode ser afetado se executar numa versão vulnerável sem mitigação adicional:
.v malicioso numa dependência possa introduzir declarações não sólidasfind_uniform_parameters em kernel/inductive.ml inspeciona apenas chamadas autorrecursivas dentro de cada corpo de um fixpoint mútuo. Quando nenhum corpo contém uma chamada autorrecursiva (todas as chamadas são chamadas cruzadas entre corpos), todos os parâmetros são marcados como uniformes. Um parâmetro que na realidade varia entre chamadas cruzadas mantém uma especificação de subtermo incorreta, permitindo que o verificador de guarda aceite uma chamada recursiva sobre um argumento que não decresce estruturalmente.
| Campo | Valor |
|---|---|
| CVE | CVE-2026-72703 |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (Alta) |
| 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édia) |
| CWE | CWE-670 — Implementação de Fluxo de Controlo Sempre Incorreta |
| Produto | Afetadas | Corrigidas |
|---|---|---|
| Rocq Prover | 8.20 – <9.2.0 | 9.2.0 |
coqchk sobre ficheiros .vo compilados como medida de defesa em profundidade.| Relatório de bug | rocq-prover/rocq#21682 |
| Correção | rocq-prover/rocq#21684 |
| Aviso VulnCheck | vulncheck.com |
| Data | Evento |
|---|---|
| 2025 | Bug reportado (rocq-prover/rocq#21682) |
| 2025 | Correção integrada (PR #21684) no Rocq 9.2.0 |
| 2026-08-24 | CVE-2026-72703 publicado pela VulnCheck |
| 2026-08-24 | PoC reproduzível em Docker publicado |