CVE-2026-72711

ملخص

نواة Lean 4 لا تتحقق من أن جسم إعلان غير شفاف مغلق. يُغفل `environment::add_opaque` استدعاء `check_no_metavar_no_fvar` الذي تنفذه مسارات التعريف والمبرهنة، لذا لا تُرفض قيمة تحتوي على متغير حر غائب عن السياق المحلي رفضًا قاطعًا. يمكن لبرنامج ميتا (metaprogram) أن يتسبب أولًا في أن تنشئ النواة محليًا مؤقتًا من النوع `False` وتسجّل نوعه في ذاكرة التخزين المؤقت للاستدلال الخاصة بمدقق الأنواع، ثم يستعيد السياق المحلي بينما يظل إدخال ذاكرة التخزين المؤقت قائمًا على نفس نسخة مدقق الأنواع، وأخيرًا يقدّم إعلانًا غير شفاف قيمته هي المتغير غير المرتبط الآن. يُجاب عن البحث في ذاكرة التخزين المؤقت قبل الفرع الذي كان سيختبر العضوية في السياق المحلي، لذا تستنتج النواة النوع المخزّن مؤقتًا وتقبل ثابتًا غير شفاف من النوع `False`، ومنه يستلزم أي قضية. يُقبل الإعلان عبر المسار المفحوص العادي عند أقصى تحقق من النواة، دون `sorry` أو `unsafeCast` أو `debug.skipKernelTC` أو `addDeclWithoutChecking` أو شيفرة أجنبية أو ملف `.olean` معدّل، ولا تحمل النتيجة أي مسلّمات (axioms). تم إصلاح ذلك في 4.32.2 بإضافة فحص الإغلاق المفقود.

المصادر

• lean-cve-poc-14484PoC

  CVE-2026-72711 — خلل في سلامة نواة Lean 4: تسميم ذاكرة التخزين المؤقت للاستدلال