CVE-2026-72703 — Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls
The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0.
Descrição oficial em inglês (tradução ainda não revisada).
Quem explora e qual a prioridade
Nota de 0 a 100 que combina exploração confirmada, uso por ransomware e grupos APT, exploits públicos, EPSS e severidade.
Como a nota foi calculada
- EPSS 0.2% (probabilidade de exploração em 30 dias)+1
- Severidade técnica (medium)+3
- CISA SSVC: exploração "poc"+5
A nota ordena a fila de correção; não substitui o contexto dos seus ativos (exposição à internet, criticidade, compensações).
Triagem
Está sendo explorada, qual a probabilidade de exploração, o que afeta e qual a severidade segundo as fontes.
Avaliação SSVC da CISA CISA
Três pontos de decisão que a CISA publica para as CVEs que avalia (SSVC 2.0.3). Uma decisão de priorização, não uma nota de severidade.
Remediação
Correções e mitigações documentadas pelas fontes — com link para o aviso original.
Nenhuma correção documentada pelas fontes consultadas. Isso não significa que não exista: verifique o aviso do fabricante.
Primeiras 24 horas
Ordenado a partir dos próprios campos do registro — exposição primeiro, porque não se corrige o que não se encontrou. Ponto de partida, gerado por regras.
- Identifique ativos expostos que executam as combinações de fabricante/produto/versão afetadas (Rocq-prover Rocq).
- Nenhuma correção documentada nas fontes: reduza a exposição e monitore o aviso do fabricante.
- A exploração exige interação do usuário: reforce filtros de e-mail/web e alerte os usuários afetados.
- Procure nos logs disponíveis sinais de tentativa de exploração compatíveis com a classe da falha (erro de lógica), erros e anomalias de autenticação.
Escopo afetado
Fabricante, produto e versões como as fontes os descrevem.
| Fabricante | Produto | Versões | Status | Fonte |
|---|---|---|---|---|
| Rocq-prover | Rocq | ≥ 8.20 e < 9.2.0 | Vulnerável | CVE Program (cve.org) e CISA ADP |
Características do ataque
O vetor CVSS decodificado. Descreve o ataque, não a sua exposição a ele.
Todas as pontuações coletadas
As fontes pontuam de forma independente e podem discordar; cada linha diz quem pontuou e em qual versão.
| Nota | Versão | Severidade | Explor. | Impacto | Pontuado por |
|---|---|---|---|---|---|
| 6.8 | CVSS 4.0 | Média | — | — | disclosure@vulncheck.com via NIST National Vulnerability Database |
| 6.8 | CVSS 4.0 | Média | — | — | VulnCheck via CVE Program (cve.org) e CISA ADP |
| 6.3 | CVSS 3.1 | Média | 1.8 | 4.0 | disclosure@vulncheck.com via NIST National Vulnerability Database |
| 6.3 | CVSS 3.1 | Média | — | — | VulnCheck via CVE Program (cve.org) e CISA ADP |
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N (nota exibida no topo: disclosure@vulncheck.com) Fraqueza MITRE
Classe de fraqueza segundo o catálogo CWE do MITRE.
EPSS ao longo do tempo FIRST
13/10/2026 → 14/10/2026 · 2 leitura(s) · máximo 0.18%
Detecção
Derivado do vetor CVSS e da classe da fraqueza. Pontos de partida, não regras testadas.
- Vetor local/físico: concentre-se em telemetria de endpoint (EDR) dos hosts afetados.
Linha do tempo
O que aconteceu com esta CVE, do mais recente ao mais antigo.
- 2026
- Produtos afetados adicionados · rocq-prover/rocq
- Avaliação SSVC atualizada
- Ficha publicada
- CVSS alterado · 6.3
- Status na fonte alterado · → Deferred
- Registro criado nesta base
- CVE publicada
Atividade das fontes
Leituras que se repetem foram contadas em vez de listadas.
- 1× Descrição oficial atualizada · 13/10/2026 – 13/10/2026
Referências
5 no registro
Em outras páginas do site
CVEs relacionadas (mesmos produtos)
- Média CVE-2026-72714 Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close 24/08/2026
- Média CVE-2026-72704 Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport 24/08/2026
- Média CVE-2026-72705 Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument 24/08/2026
Não consta em nenhuma fonte consultada
Listado em vez de deixado em branco: um campo vazio e um não medido parecem iguais na tela, e só um deles é motivo para procurar em outro lugar.
- Nenhuma versão corrigida, patch ou mitigação documentada.
- Nenhum IOC confirmado (IPs, domínios, hashes ou artefatos de malware) fornecido.
- Nenhum inventário de ativos, controle compensatório ou evidência de implantação de patch da sua organização.
- Nenhuma captura de tráfego de exploração, amostra de log ou caso de incidente.
Respondido a partir deste registro
Texto montado apenas com os campos acima — sem afirmações adicionais.
O que os defensores devem saber primeiro?
CVE-2026-72703 é "Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls", de severidade Média. Afeta Rocq (Rocq-prover); as versões estão na tabela de escopo. Não está na CISA KEV, o que não exclui exploração. CVSS 6.3 descreve a severidade técnica. EPSS 0.18% estima a probabilidade de exploração em 30 dias; nenhum dos dois substitui o contexto dos seus ativos. Verifique primeiro se ativos expostos ou críticos executam as versões afetadas, aplique as correções ou mitigações do fabricante e preserve logs para análise.
Comentários
Discussão técnica moderada. Leia as regras da comunidade.
Nenhum comentário ainda.
Entre ou crie uma conta para comentar e sugerir correções.