CVE-2026-72711 — Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable
The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::add_opaque omits the check_no_metavar_no_fvar call that the definition and theorem paths perform, so a value containing a free variable that is absent from the local context is not rejected outright. A metaprogram can first cause the kernel to create a temporary local of type False and record its type in the type checker's inference cache, then restore the local context while that cache entry persists on the same type checker instance, and finally submit an opaque declaration whose value is the now-unbound variable. The cache lookup answers before the branch that would test membership of the local context, so the kernel infers the cached type and admits an opaque constant of type False, from which any proposition follows. The declaration is accepted through the ordinary checked path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, foreign code or a modified .olean file, and the result carries no axioms. Fixed in 4.32.2 by adding the missing closure check.
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 (Leanprover Lean4).
- 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 (validação de entrada), erros e anomalias de autenticação.
Escopo afetado
Fabricante, produto e versões como as fontes os descrevem.
| Fabricante | Produto | Versões | Status | Fonte |
|---|---|---|---|---|
| Leanprover | Lean4 | < 4.32.2 | 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 · leanprover/lean4
- 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
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-72711 é "Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable", de severidade Média. Afeta Lean4 (Leanprover); 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.