CVE-2026-72711

सारांश

Lean 4 कर्नेल यह जाँच नहीं करता कि किसी अपारदर्शी (opaque) घोषणा का मुख्य भाग बंद (closed) है या नहीं। `environment::add_opaque` उस `check_no_metavar_no_fvar` कॉल को छोड़ देता है जो definition और theorem पथ निष्पादित करते हैं, इसलिए एक ऐसा मान जिसमें कोई मुक्त चर (free variable) है जो स्थानीय संदर्भ (local context) में अनुपस्थित है, सीधे अस्वीकृत नहीं होता। एक मेटाप्रोग्राम पहले कर्नेल को `False` प्रकार का एक अस्थायी स्थानीय (local) बनाने और उसके प्रकार को टाइप चेकर के inference cache में दर्ज करने का कारण बन सकता है, फिर उस स्थानीय संदर्भ को पुनर्स्थापित कर सकता है जबकि वह cache प्रविष्टि उसी टाइप चेकर इंस्टेंस पर बनी रहती है, और अंत में एक अपारदर्शी घोषणा प्रस्तुत कर सकता है जिसका मान अब अबद्ध (unbound) चर है। Cache lookup उस शाखा से पहले उत्तर देता है जो स्थानीय संदर्भ की सदस्यता का परीक्षण करती, इसलिए कर्नेल cached प्रकार का अनुमान लगाता है और `False` प्रकार के एक अपारदर्शी स्थिरांक (opaque constant) को स्वीकार कर लेता है, जिससे कोई भी प्रस्ताव (proposition) निकलता है। यह घोषणा अधिकतम कर्नेल जाँच पर सामान्य checked पथ के माध्यम से स्वीकार की जाती है, बिना `sorry`, `unsafeCast`, `debug.skipKernelTC`, `addDeclWithoutChecking`, foreign code या संशोधित `.olean` फ़ाइल के, और परिणाम में कोई axioms नहीं होते। 4.32.2 में अनुपस्थित closure जाँच जोड़कर इसे ठीक किया गया।

स्रोत

• lean-cve-poc-14484PoC

  CVE-2026-72711 — Lean 4 कर्नेल साउंडनेस बग: इन्फरेंस कैश ज़हरीलापन