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

إثبات 0 = 1 دون مسلّمات عبر تسميم ذاكرة FVar المؤقتة لإعلان غير شفاف.

الحقل	القيمة
تقرير الخلل	leanprover/lean4#14484
الإصلاح	leanprover/lean4#14498
المتأثر	Lean 4 ≤ `v4.31.0` / جميع الإصدارات السابقة
تم إصلاحه في	nightly 2026-07-23+، مع نقل الإصلاح إلى v4.32.1 وv4.33.0
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-488 (Exposure of Data Element to Wrong Session)، CWE-20 (Improper Input Validation)
CVE	CVE-2026-72711

ملخص الثغرة

مسار environment::add_opaque في نواة Lean 4 لا يستدعي check_no_metavar_no_fvar على جسم الإعلان — على عكس التعريفات والمبرهنات، التي تُجري فحص الإغلاق هذا قبل التحقق من نوع القيمة.

يستغل برنامج ميتا خبيث هذا الإغفال عبر تسميم ذاكرة الاستدلال المؤقتة:

التهيئة — تعبير نوع مُصمَّم (cachePrimingType) هو beta-redex مغلق مساوٍ تعريفياً لـ False. أثناء التحقق من نوعه، تُنشئ النواة إعلاناً محلياً مؤقتاً _kernel_fresh.2 : False وتخزّن نوعه المستنتج في ذاكرة الاستدلال المؤقتة الخاصة بنسخة type_checker.
إبطال السياق — تتم استعادة السياق المحلي (تُزال المتغيّرة المؤقتة)، لكن ذاكرة الاستدلال المؤقتة تبقى على نفس نسخة type_checker. أصبح مدخل الذاكرة المؤقتة قديماً الآن — فهو يربط معرّفاً لم يعد يشير إلى أي شيء في النطاق.
الاستغلال — قيمة الإعلان غير الشفاف هي Expr.fvar تشير إلى المعرّف القديم. يحدث البحث في الذاكرة المؤقتة قبل أن يتحقق فرع FVar من العضوية في السياق المحلي، فيُعيد False كنوع دون اكتشاف المتغيّرة غير المرتبطة إطلاقاً.

النتيجة هي ثابت غير شفاف من النوع False تقبله النواة، ومنه يُستنتج 0 = 1 بسهولة.

الاستغلال:

يستخدم فقط مسار النواة المُتحقَّق منه addDecl
يعمل مع --trust=0 (أقصى تحقق)
لا يُبلّغ عن أي مسلّمات عبر #print axioms
لا يستخدم sorry أو unsafeCast أو debug.skipKernelTC أو FFI أو التلاعب بـ .olean
يجتاز إعادة التشغيل leanchecker --fresh

الاستخدام

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

الناتج المتوقع على إصدار Lean المصاب:

[*] Running CachePoisonFalse.lean with --trust=0 ...
kernel accepted bad : False
'bad' does not depend on any axioms
'assumptionFreeFalse' does not depend on any axioms
'zero_eq_one' does not depend on any axioms

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Depends on: no axioms

    Bug class:  Inference cache poisoning (CWE-488)
    Root cause: missing check_no_metavar_no_fvar in add_opaque
    Bug report: https://github.com/leanprover/lean4/issues/14484
    Fix:        https://github.com/leanprover/lean4/pull/14498

في نسخة Lean المُرقَّعة، يرفض النواة الإعلان المعتم غير السليم النوع ويُبلِّغ السكربت بأن النسخة غير قابلة للاستغلال.

التأثير

يتأثر أي نظام يعتمد على البراهين المُتحقَّق منها بواسطة نواة Lean كحقيقة موثوقة. ويشمل ذلك:

البرمجيات المُتحقَّق منها رسميًا: المترجمات، ومكتبات التشفير، والعقود الذكية، وأنظمة الطيران، والسيارات — أي حالة سلامة مبنية على برهان Lean تكون غير صالحة إذا بُنيت بنسخة متأثرة.
البرمجيات الحاملة للبراهين (Proof-carrying code): يمكن لتبعية خبيثة في حزمة Lake أن تُدخِل بصمت إعلانات غير سليمة يستخدمها الكود اللاحق.
المدققات المستقلة: أكَّد المُبلِّغ أن إعادة التشغيل عبر leanchecker --fresh تقبل الاستغلال أيضًا. لا يمكن لصيغة التصدير comparator التعبير عن FVar، لذا فإن مسار التحقق هذا غير متأثر.
البراهين المُولَّدة بالذكاء الاصطناعي: أنظمة مثل AlphaProof وDeepSeek-Prover وKimina-Prover التي تستخدم Lean كخلفية موثوقة قد تُنتج براهين تستغل أخطاء النواة بدلًا من إثبات المبرهنات.

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

السبب الجذري

في src/kernel/environment.cpp، تتحقق الدالة add_opaque من نوع القيمة المعتمة لكنها لا تُجري فحص الإغلاق:

environment environment::add_opaque(declaration const & d, bool check) const {
    scoped_diagnostics diag(*this, check);
    opaque_val const & v = d.to_opaque_val();
    if (check) {
        type_checker checker(*this, diag.get());
        check_constant_val(*this, v.to_constant_val(), checker);
        // ← MISSING: check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
        expr val_type = checker.check(v.get_value(), v.get_lparams());
        // ...
    }
}

يستدعي كلٌّ من add_definition وadd_theorem الدالة check_no_metavar_no_fvar على قيمهما قبل التحقق من أنواعها. ويُعدّ الإغفال في add_opaque هو نقطة الدخول.

آلية تسميم ذاكرة التخزين المؤقت

تربط ذاكرة التخزين المؤقت للاستدلال في type_checker التعبيرات بأنواعها المستدلّة. وفي infer_type_core، يتم البحث في ذاكرة التخزين المؤقت:

auto it = m_infer_type_cache[binfo_idx(bi)].find(e);
if (it != m_infer_type_cache[binfo_idx(bi)].end())
    return it->second;

يُطلق قبل أن يتحقق فرع FVar من العضوية في السياق المحلي:

case expr_kind::FVar: {
    optional<local_decl> d = m_lctx.find_local_decl(e);
    if (!d) throw_kernel_exception(...);
    return d->get_type();
}

يتحكم المهاجم في تعبئة الذاكرة المؤقتة عبر تعبير النوع، مما يجعل اسم الإدخال القديم (_kernel_fresh.2) قابلاً للتنبؤ والاستهداف.

مقارنة مع #14576

الجانب	#14484 (هذا الخطأ)	#14576
فئة الخطأ	تسميم الذاكرة المؤقتة	الخلط بين الأنواع عبر التحقق من الإسقاط
نقطة الدخول	`add_opaque` يفتقد فحص الإغلاق	معاملات شبحية استقرائية متداخلة
الذاكرة المؤقتة المعنية	نعم — ذاكرة الاستدلال المؤقتة	نعم — مقارنة تجزئة التعبير
يؤثر على leanchecker	نعم	نعم
يؤثر على comparator	لا (FVar غير قابل للتعبير)	نعم

أعمال ذات صلة

endrazine/lean-cve-poc — إثبات مفهوم (PoC) لخطأ الإسقاط الاستقرائي المتداخل #14576 (بنية المستودع نفسها)
إصلاح سلامة lean4lean — تأثر lean4lean بشكل مستقل بخطأ تسميم الذاكرة المؤقتة نفسه

شكر وتقدير

اكتشاف الخطأ: Patrick Hulin (@phulin)، بمساعدة من GPT-5.6 Sol
إصلاح النواة: Joachim Breitner (@nomeata)، PR #14498
تجهيز إثبات المفهوم (PoC): Jonathan Brossard (@endrazine)

lean-cve-poc-14484

الأكثر شعبية