CVE Intelligence
Média Corrupção de memória referência de exploit

CVE-2026-72844 — Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections

The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and environment::add_inductive in src/kernel/inductive.cpp did not type check the nested inductive applications that are replaced by auxiliary types, so their parametric arguments escaped checking. A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency.

Descrição oficial em inglês (tradução ainda não revisada).

Publicada em 20/08/2026 · Atualizada em 15/10/2026 · Fontes: NIST National Vulnerability Database, CVE Program (cve.org) e CISA ADP · CNA: VulnCheck

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.

Nenhum sinal de exploração nas fontes consultadas até agora.
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.

Exploração
Não confirmada
Fora da CISA KEV — ausência de registro, não prova de que não é explorada.
EPSS FIRST
0,18%
à frente de 7% das CVEs pontuadas · 15/10/2026
Afeta
Leanprover
Lean4
CVSS base
6.3
Média · 2 fonte(s)

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.

Exploração
Prova de conceito
nenhuma · prova de conceito · ativa
Automatizável
Não
se um atacante consegue automatizar as etapas da cadeia de ataque
Impacto técnico
Parcial
parcial · controle total do componente vulnerável

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.

  1. Identifique ativos expostos que executam as combinações de fabricante/produto/versão afetadas (Leanprover Lean4).
  2. Nenhuma correção documentada nas fontes: reduza a exposição e monitore o aviso do fabricante.
  3. A exploração exige interação do usuário: reforce filtros de e-mail/web e alerte os usuários afetados.
  4. Procure nos logs disponíveis sinais de tentativa de exploração compatíveis com a classe da falha (corrupção de memória), erros e anomalias de autenticação.

Escopo afetado

Fabricante, produto e versões como as fontes os descrevem.

FabricanteProdutoVersõesStatusFonte
Leanprover Lean4 < 4.32.2versão 4.33.0-rc1 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.

Vetor de ataque
Local
Complexidade
Baixa
Privilégios exigidos
Nenhum
Interação do usuário
Necessária
Escopo
Alterado
Confidencialidade
Nenhum
Integridade
Alto
Disponibilidade
Nenhum

Todas as pontuações coletadas

As fontes pontuam de forma independente e podem discordar; cada linha diz quem pontuou e em qual versão.

NotaVersãoSeveridadeExplor.ImpactoPontuado 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.

CWE-843 · Type Confusion

Outras CVEs com esta fraqueza →

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.
  • Correlacione falhas/reinícios do serviço com tráfego de entrada; crashes repetidos podem indicar tentativas.
telemetria de endpoint (EDR)dumps de falha

Linha do tempo

O que aconteceu com esta CVE, do mais recente ao mais antigo.

  • 2026
  • Produtos afetados adicionados · leanprover/lean4
    15/10/2026 · CVE Program (cve.org) e CISA ADP
  • Avaliação SSVC atualizada
    15/10/2026 · CVE Program (cve.org) e CISA ADP
  • Ficha publicada
    15/10/2026
  • CVSS alterado · 6.3
    15/10/2026 · NIST National Vulnerability Database
  • Status na fonte alterado · → Deferred
    15/10/2026 · NIST National Vulnerability Database
  • Registro criado nesta base
    15/10/2026 · NIST National Vulnerability Database
  • CVE publicada
    20/08/2026 · VulnCheck

Atividade das fontes

Leituras que se repetem foram contadas em vez de listadas.

  • 1× Descrição oficial atualizada · 15/10/2026 – 15/10/2026

Referências

8 no registro

Em outras páginas do site

Leanprover
todas as CVEs deste fabricante
Corrupção de memória
mesma classe
CWE-843
outras páginas com esta fraqueza

CVEs relacionadas (mesmos produtos)

  • CVE-2026-72711 Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable 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-72844 é "Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections", 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.