CVE-2026-72844

Zusammenfassung

Der Lean-4-Kernel überprüft nicht, ob die in einem Projektionsausdruck benannte 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 Metaprogramm, das im Lean-Prozess läuft, kann einen falsch typisierten verschachtelten Induktiven registrieren, dessen Konstruktor eine `.proj C 0`-Projektion auf einen Wert des unzusammenhängenden Typs `W` anwendet, und der Kernel nimmt die Deklaration über den gewöhnlichen geprüften `addDecl`-Pfad bei maximaler Kernel-Prüfung an – ohne `sorry`, `unsafeCast`, `debug.skipKernelTC`, `addDeclWithoutChecking`, FFI oder eine modifizierte `.olean`-Datei. Das Ergebnis ist eine Typverwechslung, die einen Beweis von `False` ohne Axiome liefert, woraus jede Aussage abgeleitet werden kann. Der veröffentlichte Proof of Concept polstert zusätzlich zwei Ausdrücke auf, bis ihre Hashes und ungefähren Tiefen kollidieren, was den Kernel-Cache außer Kraft setzt; das ist die Technik, mit der die Schwachstelle erreicht wird, nicht ihre Ursache. Für die Ausnutzung muss ein Metaprogramm prozessintern ausgeführt werden, beispielsweise durch das Erstellen eines Projekts oder das Importieren einer bösartigen Lake-Abhängigkeit.

• lean-cve-pocPoC

  CVE-2026-72844 : Beispiel für den Beweis von "0 = 1" mithilfe einer Schwachstelle im Lean-4-Kernel.