Resumo da Vulnerabilidade

O kernel do Lean 4 não verifica se a estrutura nomeada em uma expressão de projeção corresponde ao tipo do valor que está sendo projetado, e environment::add_inductive em src/kernel/inductive.cpp não verificava os tipos das aplicações indutivas aninhadas que são substituídas por tipos auxiliares, fazendo com que seus argumentos paramétricos escapassem da verificação.

Um metaprograma em execução no processo do Lean pode registrar um indutivo aninhado com tipos incorretos cujo construtor aplica uma projeção .proj C 0 a um valor do tipo não relacionado W, e o kernel aceita a declaração pelo caminho comum verificado addDecl com verificação máxima do kernel. O resultado é uma confusão de tipos que produz uma prova de False sem carregar nenhum axioma, da qual qualquer proposição — incluindo 0 = 1 — pode ser derivada.

O exploit:

• Usa apenas o caminho verificado addDecl do kernel
• Executa com --trust=0 (verificação máxima)
• Não reporta nenhum axioma via #print axioms
• Não usa sorry, unsafeCast, debug.skipKernelTC, FFI, nem adulteração de .olean

Uso

Saída esperada em uma versão vulnerável do Lean:

Em uma versão corrigida do Lean, o kernel rejeita o indutivo com tipos incorretos e o script informa que a versão não é vulnerável.

Impacto

Qualquer sistema que confie nas provas verificadas pelo kernel do Lean como verdade absoluta é afetado. Isso inclui:

• Software verificado formalmente: compiladores, bibliotecas criptográficas, contratos inteligentes, aviônica, automotivo — qualquer caso de segurança construído sobre uma prova em Lean é inválido se for construído com uma versão afetada.
• Código portador de prova (proof-carrying code): uma dependência maliciosa em um pacote Lake pode introduzir silenciosamente declarações não sólidas que o código downstream usa.
• Verificadores independentes: foi demonstrado que a mesma classe de bug também contorna o verificador de tipos independente Nanoda.

Detalhes Técnicos

A causa raiz está no tratamento que o kernel dá aos tipos indutivos aninhados. Ao eliminar uma ocorrência aninhada I Ds is, o kernel deve verificar se os argumentos paramétricos Ds correspondem aos parâmetros declarados do indutivo. O código vulnerável não verifica se as expressões de projeção (.proj) em Ds referenciam o nome de estrutura correto — um .proj C 0 w é aceito mesmo quando w : W e W ≠ C.

Combinado com uma colisão de hash (o kernel usa comparações de Expr.hash na sua verificação de igualdade definicional), isso permite que um atacante registre declarações em que a atribuição de tipo interna do kernel diverge da semântica real do termo, levando a uma confusão de tipos e a uma prova de False.

Referências

• NVD: CVE-2026-72844
• Comunicado da VulnCheck
• Divulgação no oss-security
• Issue #14576 do Lean 4
• PR de correção #14577
• Commit de correção

Créditos

• Descoberta do bug e PoC mínima: @kiranandcode
• Exploit original do CollatzLean: @xrchz (Ramana Kumar)
• Correção do kernel: Leonardo de Moura (PR #14577)
• Registro do CVE e empacotamento do PoC: Jonathan Brossard (@endrazine)