CVE-2026-72711

Riepilogo

Il kernel di Lean 4 non verifica che il corpo di una dichiarazione opaca sia chiuso. environment::add_opaque omette la chiamata a check_no_metavar_no_fvar che i percorsi di definizione e teorema eseguono, quindi un valore contenente una variabile libera assente dal contesto locale non viene respinto immediatamente. Un metaprogramma può prima far sì che il kernel crei un locale temporaneo di tipo False e registri il suo tipo nella cache di inferenza del type checker, poi ripristinare il contesto locale mentre quella voce di cache persiste sulla stessa istanza del type checker, e infine inviare una dichiarazione opaca il cui valore è la variabile ora non vincolata. La ricerca nella cache risponde prima del ramo che verificherebbe l'appartenenza al contesto locale, quindi il kernel inferisce il tipo memorizzato nella cache e ammette una costante opaca di tipo False, dalla quale segue qualsiasi proposizione. La dichiarazione viene accettata attraverso il normale percorso verificato con il massimo livello di controllo del kernel, senza sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, codice foreign o un file .olean modificato, e il risultato non porta assiomi. Corretto in 4.32.2 aggiungendo il controllo di chiusura mancante.

Fonti

• lean-cve-poc-14484PoC

  CVE-2026-72711 — Bug di correttezza del kernel di Lean 4: avvelenamento della cache di inferenza