CVE-2026-72844

सारांश

Lean 4 कर्नेल यह सत्यापित नहीं करता कि किसी प्रोजेक्शन अभिव्यक्ति में नामित संरचना प्रोजेक्ट किए जा रहे मान के प्रकार से मेल खाती है, और src/kernel/inductive.cpp में environment::add_inductive उन नेस्टेड इंडक्टिव अनुप्रयोगों की टाइप जाँच नहीं करता था जिन्हें सहायक प्रकारों द्वारा प्रतिस्थापित किया जाता है, जिससे उनके पैरामीट्रिक तर्क जाँच से बच गए। Lean प्रक्रिया में चलने वाला एक मेटाप्रोग्राम एक गलत-टाइप वाला नेस्टेड इंडक्टिव पंजीकृत कर सकता है जिसका कंस्ट्रक्टर असंबंधित प्रकार W के मान पर .proj C 0 प्रोजेक्शन लागू करता है, और कर्नेल अधिकतम कर्नेल जाँच पर सामान्य checked addDecl पथ के माध्यम से घोषणा को स्वीकार कर लेता है, बिना sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, या किसी संशोधित .olean फ़ाइल के। परिणाम एक प्रकार का भ्रम है जो False का एक प्रमाण उत्पन्न करता है जिसमें कोई अभिगृहीत नहीं होता, जिससे कोई भी प्रस्ताव व्युत्पन्न किया जा सकता है। प्रकाशित प्रूफ ऑफ कॉन्सेप्ट अतिरिक्त रूप से दो अभिव्यक्तियों को तब तक पैड करता है जब तक कि उनके हैश और अनुमानित गहराइयाँ टकरा नहीं जातीं, जो कर्नेल कैशिंग को विफल कर देता है; यह त्रुटि तक पहुँचने के लिए उपयोग की जाने वाली तकनीक है, इसका कारण नहीं। शोषण के लिए किसी मेटाप्रोग्राम को इन-प्रोसेस चलाना आवश्यक है, उदाहरण के लिए किसी प्रोजेक्ट का निर्माण करके या किसी दुर्भावनापूर्ण Lake निर्भरता को आयात करके।

• lean-cve-pocPoC

  CVE-2026-72844 : Lean 4 कर्नेल में एक कमजोरी का उपयोग करके "0 = 1" सिद्ध करने का उदाहरण।