CVE-2026-72844

Riepilogo

Il kernel di Lean 4 non verifica che la struttura indicata in un'espressione di proiezione corrisponda al tipo del valore su cui viene applicata la proiezione, e environment::add_inductive in src/kernel/inductive.cpp non eseguiva il type check delle applicazioni induttive annidate che vengono sostituite da tipi ausiliari, lasciando così sfuggire i loro argomenti parametrici alla verifica. Un metaprogramma eseguito nel processo Lean può registrare un'induttiva annidata mal tipizzata il cui costruttore applica una proiezione .proj C 0 a un valore del tipo non correlato W, e il kernel ammette la dichiarazione attraverso il normale percorso addDecl con verifica, al livello massimo di controllo del kernel, senza ricorrere a sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI o a un file .olean modificato. Il risultato è una confusione di tipi che produce una dimostrazione di False priva di assiomi, da cui si può derivare qualsiasi proposizione. Il proof of concept pubblicato aggiunge inoltre padding a due espressioni finché i loro hash e le profondità approssimative non collidono, aggirando la cache del kernel; si tratta della tecnica usata per raggiungere la falla, non della sua causa. Lo sfruttamento richiede l'esecuzione di un metaprogramma in-process, ad esempio compilando un progetto o importando una dipendenza Lake dannosa.

• lean-cve-pocPoC

  CVE-2026-72844 : Esempio di dimostrazione di "0 = 1" utilizzando una vulnerabilità nel kernel di Lean 4.