endrazine/lean-cve-pocCVE-2026-72844 : Beispiel für den Beweis von "0 = 1" mithilfe einer Schwachstelle im Lean-4-Kernel.
Axiomfreier Beweis von 0 = 1 durch Umgehung der Projektionsvalidierung bei verschachtelten induktiven Typen.
| Feld | Wert |
|---|
| CVE | CVE-2026-72844 |
| Advisory | VulnCheck VCSA |
| Bug-Report | leanprover/lean4#14576 |
| Fix | leanprover/lean4#14577 |
| Betroffen | Lean 4 ≤ v4.31.0 / nightly ≤ 2026-07-27 |
| Behoben 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 MEDIUM |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 6.3 MEDIUM |
| CWE | CWE-843 (Typverwechslung) |
Der Lean-4-Kernel prüft nicht, ob die in einem Projektionsausdruck genannte Struktur mit dem Typ des projizierten Werts übereinstimmt, und environment::add_inductive in src/kernel/inductive.cpp führte keine Typprüfung der verschachtelten induktiven Anwendungen durch, die durch Hilfstypen ersetzt werden, sodass ihre parametrischen Argumente der Prüfung entgingen.
Ein im Lean-Prozess laufendes Metaprogramm kann einen falsch typisierten verschachtelten induktiven Typ registrieren, dessen Konstruktor eine .proj C 0-Projektion auf einen Wert des fremden Typs W anwendet, und der Kernel akzeptiert die Deklaration über den normalen geprüften addDecl-Pfad bei maximaler Kernel-Prüfung. Das Ergebnis ist eine Typverwechslung, die einen Beweis von False ohne Axiome liefert, woraus jede Aussage — einschließlich 0 = 1 — abgeleitet werden kann.
Der Exploit:
addDecl-Kernelpfad--trust=0 (maximale Prüfung)#print axiomssorry, unsafeCast, debug.skipKernelTC, FFI noch .olean-Manipulationdocker build -t lean-cve-poc .
docker run --rm lean-cve-poc
Erwartete Ausgabe auf einer verwundbaren Lean-Version:
[*] 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
Auf einer gepatchten Lean-Version weist der Kernel den falsch typisierten induktiven Typ zurück, und das Skript meldet, dass die Version nicht verwundbar ist.
Jedes System, das den kernel-geprüften Beweisen von Lean als Grundwahrheit vertraut, ist betroffen. Dazu gehören:
Die Ursache liegt in der Behandlung verschachtelter induktiver Typen durch den Kernel. Beim Eliminieren eines verschachtelten Vorkommens I Ds is muss der Kernel prüfen, ob die parametrischen Argumente Ds mit den deklarierten Parametern des induktiven Typs übereinstimmen. Der verwundbare Code prüft nicht, ob Projektionsausdrücke (.proj) in Ds auf den korrekten Strukturnamen verweisen — ein .proj C 0 w wird selbst dann akzeptiert, wenn w : W und W ≠ C.
In Kombination mit einer Hash-Kollision (der Kernel verwendet Expr.hash-Vergleiche bei seiner definitionalen Gleichheitsprüfung) ermöglicht dies einem Angreifer, Deklarationen zu registrieren, bei denen die interne Typzuweisung des Kernels von der tatsächlichen Term-Semantik abweicht, was zu Typverwechslung und einem Beweis von False führt.