CVE-2026-72844: خطأ سلامة نواة Lean 4

إثبات 0 = 1 بدون مسلمات عبر تجاوز التحقق من الإسقاطات الاستقرائية المتداخلة.

ملخص الثغرة

لا تتحقق نواة Lean 4 من أن البنية المذكورة في تعبير الإسقاط تطابق نوع القيمة التي يجري إسقاطها، كما أن environment::add_inductive في src/kernel/inductive.cpp لم يتحقق من الأنواع للتطبيقات الاستقرائية المتداخلة التي تُستبدل بأنواع مساعدة، لذا فإن وسائطها البارامترية تجاوزت الفحص.

يمكن لبرنامج ميتا يعمل داخل عملية Lean تسجيل استقرائي متداخل خاطئ الأنواع، بحيث يطبّق مُنشئه إسقاط .proj C 0 على قيمة من النوع غير المرتبط W، وتقبل النواة التصريح عبر مسار addDecl المُفحَص العادي بأقصى درجة فحص في النواة. النتيجة هي خلط أنواع ينتج برهانًا على False لا يحمل أي مسلمات، ويمكن اشتقاق أي افتراض — بما في ذلك 0 = 1 — منه.

الاستغلال:

• يستخدم فقط مسار النواة المُفحَص 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 تكون غير صالحة إذا بُنيت بإصدار متأثر.
• الكود الحامل للبراهين: يمكن لاعتمادية خبيثة في حزمة Lake أن تُدخل بصمت تصريحات غير سليمة يستخدمها الكود اللاحق.
• المدققات المستقلة: تبيّن أن نفس فئة الخطأ تتجاوز أيضًا المدقق النوعي المستقل Nanoda.

التفاصيل التقنية

السبب الجذري يكمن في معالجة النواة للأنواع الاستقرائية المتداخلة. عند حذف حدوث متداخل I Ds is، يجب على النواة التحقق من أن الوسائط البارامترية Ds تطابق المعاملات المعلنة للاستقرائي. الكود المعرّض للثغرة يفشل في التحقق من أن تعبيرات الإسقاط (.proj) في Ds تشير إلى اسم البنية الصحيح — حيث يُقبل .proj C 0 w حتى عندما w : W و W ≠ C.

وبالاقتران مع تصادم تجزئة (تستخدم النواة مقارنات Expr.hash في فحص المساواة التعريفية)، يسمح ذلك للمهاجم بتسجيل تصريحات يتعارض فيها إسناد الأنواع الداخلي للنواة مع الدلالات الفعلية للمصطلح، مما يؤدي إلى خلط الأنواع وبرهان على False.

المراجع

• NVD: CVE-2026-72844
• استشارة VulnCheck
• إفصاح oss-security
• مشكلة Lean 4 #14576
• إصلاح PR #14577
• إصلاح commit

الاعتمادات

• اكتشاف الخطأ وإثبات المفهوم المصغّر: @kiranandcode
• استغلال CollatzLean الأصلي: @xrchz (Ramana Kumar)
• إصلاح النواة: Leonardo de Moura (PR #14577)
• تسجيل CVE وتغليف إثبات المفهوم: Jonathan Brossard (@endrazine)