CVE-2026-72844: Lean 4 कर्नेल साउंडनेस बग

नेस्टेड इंडक्टिव प्रोजेक्शन वैलिडेशन बायपास के माध्यम से एक्सिओम-मुक्त 0 = 1 सिद्ध करना।

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

Lean 4 कर्नेल यह सत्यापित नहीं करता कि प्रोजेक्शन एक्सप्रेशन में नामित संरचना प्रोजेक्ट किए जा रहे मान के प्रकार से मेल खाती है, और src/kernel/inductive.cpp में environment::add_inductive उन नेस्टेड इंडक्टिव अनुप्रयोगों का टाइप चेक नहीं करता था जिन्हें सहायक प्रकारों द्वारा प्रतिस्थापित किया जाता है, जिससे उनके पैरामीट्रिक तर्क जाँच से बच निकलते थे।

Lean प्रक्रिया में चल रहा एक मेटाप्रोग्राम एक गलत-टाइप किया गया नेस्टेड इंडक्टिव पंजीकृत कर सकता है जिसका कंस्ट्रक्टर असंबंधित प्रकार W के मान पर .proj C 0 प्रोजेक्शन लागू करता है, और कर्नेल अधिकतम कर्नेल जाँच पर सामान्य checked addDecl पथ के माध्यम से घोषणा को स्वीकार कर लेता है। इसका परिणाम एक टाइप कन्फ्यूज़न होता है जो बिना किसी एक्सिओम के False का प्रमाण देता है, जिससे कोई भी प्रस्ताव — जिसमें 0 = 1 भी शामिल है — निकाला जा सकता है।

शोषण (एक्सप्लॉइट):

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

उपयोग

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

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

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

पैच किए गए Lean संस्करण पर, कर्नेल गलत-टाइप वाले इंडक्टिव को अस्वीकार कर देता है और स्क्रिप्ट रिपोर्ट करती है कि संस्करण भेद्य नहीं है।

प्रभाव

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

• औपचारिक रूप से सत्यापित सॉफ़्टवेयर: कंपाइलर, क्रिप्टोग्राफ़िक लाइब्रेरी, स्मार्ट कॉन्ट्रैक्ट, एवियोनिक्स, ऑटोमोटिव — Lean प्रमाण पर निर्मित कोई भी सुरक्षा केस अमान्य है यदि वह प्रभावित संस्करण के साथ बनाया गया है।
• प्रमाण-वाहक कोड (Proof-carrying code): Lake पैकेज में एक दुर्भावनापूर्ण निर्भरता चुपचाप असाउंड घोषणाएँ पेश कर सकती है जिनका नीचे की ओर का कोड उपयोग करता है।
• स्वतंत्र जाँचकर्ता: यह दिखाया गया था कि बग का यही वर्ग Nanoda स्वतंत्र टाइप चेकर को भी बायपास कर देता है।

तकनीकी विवरण

मूल कारण नेस्टेड इंडक्टिव प्रकारों के प्रति कर्नेल की हैंडलिंग में है। किसी नेस्टेड घटना I Ds is को समाप्त करते समय, कर्नेल को यह सत्यापित करना चाहिए कि पैरामीट्रिक तर्क Ds इंडक्टिव के घोषित पैरामीटर्स से मेल खाते हैं। भेद्य कोड यह जाँचने में विफल रहता है कि Ds में प्रोजेक्शन एक्सप्रेशन (.proj) सही संरचना नाम को संदर्भित करते हैं — एक .proj C 0 w तब भी स्वीकार किया जाता है जब w : W और W ≠ C हो।

हैश कोलिज़न के साथ संयुक्त रूप से (कर्नेल अपनी परिभाषात्मक समानता जाँच में Expr.hash तुलनाओं का उपयोग करता है), यह एक हमलावर को ऐसी घोषणाएँ पंजीकृत करने की अनुमति देता है जहाँ कर्नेल का आंतरिक प्रकार असाइनमेंट वास्तविक टर्म सेमेंटिक्स से असहमत होता है, जिससे टाइप कन्फ्यूज़न और False का प्रमाण उत्पन्न होता है।

संदर्भ

• NVD: CVE-2026-72844
• VulnCheck परामर्श
• oss-security प्रकटीकरण
• Lean 4 समस्या #14576
• फिक्स PR #14577
• फिक्स कमिट

श्रेय

• बग की खोज और न्यूनतम PoC: @kiranandcode
• मूल CollatzLean शोषण: @xrchz (रमण कुमार)
• कर्नेल फिक्स: Leonardo de Moura (PR #14577)
• CVE दाखिल करना और PoC पैकेजिंग: Jonathan Brossard (@endrazine)