CVE-2026-72844

ملخص

نواة Lean 4 لا تتحقق من أن البنية المذكورة في تعبير الإسقاط (projection expression) تطابق نوع القيمة التي يتم إسقاطها، كما أن environment::add_inductive في src/kernel/inductive.cpp لم يقم بفحص أنواع تطبيقات الاستقراء المتداخلة (nested inductive applications) التي يتم استبدالها بأنواع مساعدة، لذا فإن وسائطها البارامترية لم تخضع للفحص. يمكن لبرنامج ميتا (metaprogram) يعمل داخل عملية Lean أن يسجّل استقراءً متداخلاً سيئ الأنواع (ill-typed nested inductive) بحيث يطبّق مُنشئه إسقاطاً .proj C 0 على قيمة من النوع غير المرتبط W، وتقبل النواة الإعلان عبر مسار addDecl المُفحَص العادي عند أقصى إعدادات فحص النواة، دون استخدام sorry أو unsafeCast أو debug.skipKernelTC أو addDeclWithoutChecking أو FFI أو ملف .olean معدّل. النتيجة هي خلط في الأنواع (type confusion) ينتج عنه برهان على False لا يحمل أي بديهيات (axioms)، ومنه يمكن اشتقاق أي قضية (proposition). إثبات المفهوم (proof of concept) المنشور يقوم أيضاً بحشو تعبيرين حتى تتصادم قيم التجزئة (hashes) والأعماق التقريبية، مما يبطل التخزين المؤقت للنواة؛ وهذه هي التقنية المستخدمة للوصول إلى الثغرة، وليست سببها. يتطلب استغلال الثغرة تشغيل برنامج ميتا داخل العملية (in-process)، على سبيل المثال عبر بناء مشروع أو استيراد اعتماد Lake خبيث.

• lean-cve-pocPoC

  CVE-2026-72844 : مثال على إثبات "0 = 1" باستخدام ثغرة في نواة Lean 4.