CVE-2026-72711 — Lean 4 Kernel-Soundness-Fehler: Vergiftung des Inferenz-Caches

Axiomfreier Beweis von 0 = 1 durch Vergiftung des FVar-Caches mittels opaker Deklaration.

Feld	Wert
Fehlerbericht	leanprover/lean4#14484
Fix	leanprover/lean4#14498
Betroffen	Lean 4 ≤ `v4.31.0` / alle früheren Versionen
Behoben in	nightly 2026-07-23+, zurückportiert auf v4.32.1 und v4.33.0
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-488 (Exposure of Data Element to Wrong Session), CWE-20 (Improper Input Validation)
CVE	CVE-2026-72711

Zusammenfassung der Schwachstelle

Der Pfad environment::add_opaque des Lean-4-Kernels ruft check_no_metavar_no_fvar nicht für den Deklarationskörper auf — anders als bei Definitionen und Theoremen, die diese Abschlussprüfung vor der Typprüfung des Werts durchführen.

Ein gegnerisches Metaprogramm nutzt diese Auslassung durch Vergiftung des Inferenz-Caches aus:

Vorbereitung (Priming) — Ein präparierter Typausdruck (cachePrimingType) ist eine geschlossene Beta-Redex, die definitionell gleich False ist. Während der Typprüfung erzeugt der Kernel eine temporäre lokale Deklaration _kernel_fresh.2 : False und speichert deren abgeleiteten Typ im Inferenz-Cache der type_checker-Instanz.
Kontextinvalidierung — Der lokale Kontext wird wiederhergestellt (die temporäre Variable wird entfernt), aber der Inferenz-Cache bleibt auf derselben type_checker-Instanz bestehen. Der Cache-Eintrag ist nun veraltet — er ordnet einen Bezeichner zu, der sich nicht mehr auf etwas im Gültigkeitsbereich bezieht.
Ausnutzung — Der Wert der opaken Deklaration ist ein Expr.fvar, der auf den veralteten Bezeichner zeigt. Die Cache-Suche erfolgt bevor der FVar-Zweig die Zugehörigkeit zum lokalen Kontext prüft, und gibt False als Typ zurück, ohne jemals die ungebundene Variable zu erkennen.

Das Ergebnis ist eine vom Kernel akzeptierte opake Konstante vom Typ False, aus der 0 = 1 trivial folgt.

Der Exploit:

Verwendet ausschließlich den geprüften addDecl-Kernelpfad
Läuft mit --trust=0 (maximale Prüfung)
Meldet keine Axiome über #print axioms
Verwendet kein sorry, unsafeCast, debug.skipKernelTC, FFI oder .olean-Manipulation
Besteht die leanchecker --fresh-Wiedergabe

Verwendung

docker build -t lean-cve-poc-14484 .
docker run --rm lean-cve-poc-14484

Erwartete Ausgabe bei einer verwundbaren Lean-Version:

[*] Running CachePoisonFalse.lean with --trust=0 ...
kernel accepted bad : False
'bad' does not depend on any axioms
'assumptionFreeFalse' does not depend on any axioms
'zero_eq_one' does not depend on any axioms

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Depends on: no axioms

    Bug class:  Inference cache poisoning (CWE-488)
    Root cause: missing check_no_metavar_no_fvar in add_opaque
    Bug report: https://github.com/leanprover/lean4/issues/14484
    Fix:        https://github.com/leanprover/lean4/pull/14498

In einer gepatchten Lean-Version lehnt der Kernel die falsch typisierte opake Deklaration ab und das Skript meldet, dass die Version nicht anfällig ist.

Auswirkungen

Jedes System, das die kernel-geprüften Beweise von Lean als Grundwahrheit vertraut, ist betroffen. Dazu gehören:

Formal verifizierte Software: Compiler, kryptografische Bibliotheken, Smart Contracts, Avionik, Automotive — jede Sicherheitsargumentation, die auf einem Lean-Beweis aufbaut, ist ungültig, wenn sie mit einer betroffenen Version erstellt wurde.
Proof-Carrying Code: Eine bösartige Abhängigkeit in einem Lake-Paket kann stillschweigend ungesunde Deklarationen einführen, die nachgelagerter Code verwendet.
Unabhängige Checker: Der Melder bestätigte, dass die Wiedergabe mit leanchecker --fresh den Exploit ebenfalls akzeptiert. Das Exportformat von comparator kann kein FVar ausdrücken, daher ist dieser Validierungspfad nicht betroffen.
KI-generierte Beweise: Systeme wie AlphaProof, DeepSeek-Prover und Kimina-Prover, die Lean als vertrauenswürdiges Backend verwenden, könnten Beweise erzeugen, die Kernel-Fehler ausnutzen, anstatt Theoreme zu beweisen.

Technische Details

Ursache

In src/kernel/environment.cpp prüft die Funktion add_opaque den Typ des opaken Werts, führt jedoch keine Closure-Prüfung durch:

environment environment::add_opaque(declaration const & d, bool check) const {
    scoped_diagnostics diag(*this, check);
    opaque_val const & v = d.to_opaque_val();
    if (check) {
        type_checker checker(*this, diag.get());
        check_constant_val(*this, v.to_constant_val(), checker);
        // ← MISSING: check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
        expr val_type = checker.check(v.get_value(), v.get_lparams());
        // ...
    }
}

Sowohl add_definition als auch add_theorem rufen check_no_metavar_no_fvar auf ihren Werten auf, bevor sie typgeprüft werden. Die Auslassung in add_opaque ist der Einstiegspunkt.

Cache-Poisoning-Mechanismus

Der Inferenz-Cache in type_checker ordnet Ausdrücke ihren inferierten Typen zu. In infer_type_core erfolgt der Cache-Lookup:

auto it = m_infer_type_cache[binfo_idx(bi)].find(e);
if (it != m_infer_type_cache[binfo_idx(bi)].end())
    return it->second;

fires bevor der FVar-Zweig die Zugehörigkeit zum lokalen Kontext validiert:

case expr_kind::FVar: {
    optional<local_decl> d = m_lctx.find_local_decl(e);
    if (!d) throw_kernel_exception(...);
    return d->get_type();
}

Der Angreifer kontrolliert die Cache-Befüllung über den Typausdruck und macht dadurch den Namen des veralteten Eintrags (_kernel_fresh.2) vorhersehbar und angreifbar.

Vergleich mit #14576

Aspekt	#14484 (dieser Bug)	#14576
Fehlerklasse	Cache-Poisoning	Typverwechslung durch Projektionsvalidierung
Einstiegspunkt	`add_opaque` fehlende Closure-Prüfung	Verschachtelte induktive Phantom-Parameter
Beteiligter Cache	Ja — Inferenz-Cache	Ja — Ausdrucks-Hash-Vergleich
Betrifft leanchecker	Ja	Ja
Betrifft comparator	Nein (FVar nicht ausdrückbar)	Ja

Danksagungen

Fehlerentdeckung: Patrick Hulin (@phulin), mit Unterstützung von GPT-5.6 Sol
Kernel-Fix: Joachim Breitner (@nomeata), PR #14498
PoC-Paketierung: Jonathan Brossard (@endrazine)

lean-cve-poc-14484

Beliebteste