CVE-2026-72711

Resumo

O kernel Lean 4 não verifica se o corpo de uma declaração opaca é fechado. environment::add_opaque omite a chamada check_no_metavar_no_fvar que os caminhos de definição e teorema executam, portanto um valor contendo uma variável livre ausente do contexto local não é rejeitado de imediato. Um metaprograma pode primeiro fazer com que o kernel crie um local temporário do tipo False e registre seu tipo no cache de inferência do verificador de tipos, depois restaurar o contexto local enquanto essa entrada de cache persiste na mesma instância do verificador de tipos e, por fim, submeter uma declaração opaca cujo valor é a variável agora não vinculada. A consulta ao cache responde antes do ramo que testaria a pertinência ao contexto local, de modo que o kernel infere o tipo em cache e admite uma constante opaca do tipo False, a partir da qual qualquer proposição se segue. A declaração é aceita pelo caminho verificado comum com verificação máxima do kernel, sem sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, código estrangeiro ou um arquivo .olean modificado, e o resultado não carrega axiomas. Corrigido em 4.32.2 ao adicionar a verificação de fechamento ausente.

Fontes

• lean-cve-poc-14484PoC

  CVE-2026-72711 — Bug de solidez do kernel do Lean 4: Envenenamento do cache de inferência