CVE-2026-72711 — Lean 4 Kernel Soundness Bug: Inference Cache Poisoning

अपारदर्शी घोषणा FVar कैश ज़हरीकरण के माध्यम से स्वयंसिद्ध-मुक्त रूप से 0 = 1 सिद्ध करना।

Field	Value
Bug report	leanprover/lean4#14484
Fix	leanprover/lean4#14498
Affected	Lean 4 ≤ `v4.31.0` / all prior versions
Fixed in	nightly 2026-07-23+, backported to v4.32.1 and 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

भेद्यता सारांश

Lean 4 कर्नेल का environment::add_opaque पथ घोषणा निकाय पर check_no_metavar_no_fvar को कॉल नहीं करता — परिभाषाओं और प्रमेयों के विपरीत, जो मान को टाइप-चेक करने से पहले यह क्लोज़र जाँच करते हैं।

एक विरोधी मेटाप्रोग्राम अनुमान कैश ज़हरीकरण के माध्यम से इस चूक का शोषण करता है:

प्राइमिंग — एक तैयार किया गया टाइप व्यंजक (cachePrimingType) एक बंद बीटा-रेडेक्स है जो परिभाषात्मक रूप से False के बराबर है। इसे टाइप-चेक करते समय, कर्नेल एक अस्थायी स्थानीय घोषणा _kernel_fresh.2 : False बनाता है और इसके अनुमानित टाइप को type_checker इंस्टेंस के अनुमान कैश में कैश करता है।
संदर्भ अमान्यकरण — स्थानीय संदर्भ बहाल कर दिया जाता है (अस्थायी चर हटा दिया जाता है), लेकिन अनुमान कैश उसी type_checker इंस्टेंस पर बना रहता है। कैश प्रविष्टि अब पुरानी है — यह एक ऐसे पहचानकर्ता को मैप करती है जो अब किसी भी स्कोप में संदर्भित नहीं है।
शोषण — अपारदर्शी घोषणा का मान एक Expr.fvar है जो पुराने पहचानकर्ता की ओर इंगित करता है। कैश लुकअप इससे पहले सक्रिय होता है कि FVar शाखा स्थानीय-संदर्भ सदस्यता की जाँच करे, और बिना कभी असंबद्ध चर का पता लगाए टाइप के रूप में False लौटाता है।

परिणाम एक कर्नेल-स्वीकृत अपारदर्शी स्थिरांक है जिसका टाइप False है, जिससे 0 = 1 तुच्छ रूप से निकलता है।

शोषण:

केवल जाँचे गए addDecl कर्नेल पथ का उपयोग करता है
--trust=0 (अधिकतम जाँच) के साथ चलता है
#print axioms के माध्यम से कोई स्वयंसिद्ध रिपोर्ट नहीं करता
किसी भी sorry, unsafeCast, debug.skipKernelTC, FFI, या .olean छेड़छाड़ का उपयोग नहीं करता
leanchecker --fresh रीप्ले पास करता है

उपयोग

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

एक असुरक्षित Lean संस्करण पर अपेक्षित आउटपुट:

[*] 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

पैच किए गए Lean संस्करण पर, कर्नेल दोषपूर्ण-टाइप वाली अपारदर्शी घोषणा को अस्वीकार कर देता है और स्क्रिप्ट रिपोर्ट करती है कि संस्करण असुरक्षित नहीं है।

प्रभाव

कोई भी सिस्टम जो Lean के कर्नेल-जाँचे गए प्रमाणों को सत्य मानता है, प्रभावित है। इसमें शामिल हैं:

औपचारिक रूप से सत्यापित सॉफ़्टवेयर: कंपाइलर, क्रिप्टोग्राफ़िक लाइब्रेरी, स्मार्ट कॉन्ट्रैक्ट, एवियोनिक्स, ऑटोमोटिव — Lean प्रमाण पर बना कोई भी सुरक्षा मामला अमान्य है यदि इसे प्रभावित संस्करण के साथ बनाया गया हो।
प्रमाण-वाहक कोड: Lake पैकेज में एक दुर्भावनापूर्ण निर्भरता चुपचाप अविश्वसनीय घोषणाएँ पेश कर सकती है जिनका उपयोग डाउनस्ट्रीम कोड करता है।
स्वतंत्र जाँचकर्ता: रिपोर्टर ने पुष्टि की कि leanchecker --fresh रीप्ले भी एक्सप्लॉइट को स्वीकार करता है। comparator एक्सपोर्ट फ़ॉर्मेट एक FVar को व्यक्त नहीं कर सकता, इसलिए वह सत्यापन पथ अप्रभावित है।
AI-जनित प्रमाण: AlphaProof, DeepSeek-Prover, और Kimina-Prover जैसे सिस्टम जो Lean को एक विश्वसनीय बैकएंड के रूप में उपयोग करते हैं, ऐसे प्रमाण उत्पन्न कर सकते हैं जो प्रमेय सिद्ध करने के बजाय कर्नेल बग का शोषण करते हैं।

तकनीकी विवरण

मूल कारण

src/kernel/environment.cpp में, add_opaque फ़ंक्शन अपारदर्शी मान के प्रकार की जाँच करता है लेकिन क्लोज़र जाँच नहीं करता:

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());
        // ...
    }
}

add_definition और add_theorem दोनों अपने मानों को type-check करने से पहले उन पर check_no_metavar_no_fvar कॉल करते हैं। add_opaque में यह चूक प्रवेश बिंदु है।

कैश पॉइज़निंग तंत्र

type_checker में inference cache व्यंजकों को उनके अनुमानित प्रकारों से मैप करता है। infer_type_core में, कैश लुकअप:

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

FVar शाखा स्थानीय-संदर्भ सदस्यता को मान्य करने से पहले सक्रिय होता है:

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

हमलावर टाइप एक्सप्रेशन के माध्यम से कैश पॉप्युलेशन को नियंत्रित करता है, जिससे स्टेल एंट्री का नाम (_kernel_fresh.2) पूर्वानुमेय और लक्षित करने योग्य हो जाता है।

#14576 के साथ तुलना

पहलू	#14484 (यह बग)	#14576
बग वर्ग	कैश पॉइज़निंग	प्रोजेक्शन वैलिडेशन के माध्यम से टाइप कन्फ्यूज़न
प्रवेश बिंदु	`add_opaque` में क्लोज़र जाँच अनुपस्थित	नेस्टेड इंडक्टिव फैंटम पैरामीटर
कैश शामिल	हाँ — इन्फरेंस कैश	हाँ — expr हैश तुलना
leanchecker को प्रभावित करता है	हाँ	हाँ
comparator को प्रभावित करता है	नहीं (FVar व्यक्त करने योग्य नहीं)	हाँ

श्रेय

बग की खोज: Patrick Hulin (@phulin), GPT-5.6 Sol की सहायता से
कर्नेल फिक्स: Joachim Breitner (@nomeata), PR #14498
PoC पैकेजिंग: Jonathan Brossard (@endrazine)

lean-cve-poc-14484

सबसे लोकप्रिय