endrazine/lean-cve-pocCVE-2026-72844 : Esempio di dimostrazione di "0 = 1" utilizzando una vulnerabilità nel kernel di Lean 4.
Dimostrare 0 = 1 senza assiomi tramite bypass della validazione delle proiezioni induttive annidate.
| Field | Value |
|---|
| CVE | CVE-2026-72844 |
| Advisory | VulnCheck VCSA |
| Bug report | leanprover/lean4#14576 |
| Fix | leanprover/lean4#14577 |
| Affected | Lean 4 ≤ v4.31.0 / nightly ≤ 2026-07-27 |
| Fixed in | nightly 2026-07-29+ / v4.32.2 |
| CVSS 4.0 | AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N — 6.8 MEDIO |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 6.3 MEDIO |
| CWE | CWE-843 (Confusione di tipo) |
Il kernel di Lean 4 non verifica che la struttura nominata in un'espressione
di proiezione corrisponda al tipo del valore su cui viene effettuata la
proiezione, e environment::add_inductive in src/kernel/inductive.cpp non
eseguiva il controllo di tipo sulle applicazioni induttive annidate che
vengono sostituite da tipi ausiliari, quindi i loro argomenti parametrici
sfuggivano al controllo.
Un metaprogramma in esecuzione nel processo Lean può registrare un tipo
induttivo annidato mal tipizzato il cui costruttore applica una proiezione
.proj C 0 a un valore del tipo non correlato W, e il kernel accetta la
dichiarazione tramite il normale percorso controllato addDecl al massimo
livello di controllo del kernel. Il risultato è una confusione di tipo che
produce una dimostrazione di False senza assiomi, dalla quale è possibile
derivare qualsiasi proposizione, inclusa 0 = 1.
L'exploit:
addDecl controllato--trust=0 (controllo massimo)#print axiomssorry, unsafeCast, debug.skipKernelTC, FFI o manomissione di .oleandocker build -t lean-cve-poc .
docker run --rm lean-cve-poc
Output atteso su una versione vulnerabile di Lean:
[*] Running ZeroEqOne.lean with --trust=0 ...
'bad' does not depend on any axioms
'boom' does not depend on any axioms
'zero_eq_one' does not depend on any axioms
zero_eq_one : 0 = 1
[!] VULNERABILITY CONFIRMED — CVE-2026-72844
zero_eq_one : 0 = 1
Depends on: no axioms
Su una versione corretta di Lean, il kernel rifiuta il tipo induttivo mal tipizzato e lo script segnala che la versione non è vulnerabile.
Qualsiasi sistema che consideri le dimostrazioni verificate dal kernel di Lean come verità di riferimento è interessato. Ciò include:
La causa principale risiede nella gestione da parte del kernel dei tipi
induttivi annidati. Quando si elimina un'occorrenza annidata I Ds is, il
kernel deve verificare che gli argomenti parametrici Ds corrispondano ai
parametri dichiarati del tipo induttivo. Il codice vulnerabile non controlla
che le espressioni di proiezione (.proj) in Ds facciano riferimento al
nome della struttura corretto — un .proj C 0 w viene accettato anche quando
w : W e W ≠ C.
Combinato con una collisione di hash (il kernel usa confronti Expr.hash
nel suo controllo di uguaglianza definizionale), ciò consente a un attaccante
di registrare dichiarazioni in cui l'assegnazione interna dei tipi del kernel
non concorda con la semantica effettiva del termine, portando a una confusione
di tipo e a una dimostrazione di False.