CVE-2026-72705 — Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument
The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments are not tracked. This admits a type that is definitionally equal to its own negation, so self-application produces False in purely definitional code, without tactics, axioms, plugins or unsafe flags, and Print Assumptions reports the result as closed under the global context. 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 | < 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-72703 Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls 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-72705 é "Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument", 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.