CVE-2026-72704

ملخص

مدقق الحماية في Rocq Prover لا يعيد فحص التمثيل الشجري العودي لمعامل نوع استقرائي بعد أن تغيّر ذلك المعامل بواسطة النقل. قد تطبّق نقطة ثابتة إعادة كتابة على طول تساوٍ بين الأنواع على وسيطها العودي، وهو ما يقبله مدقق الحماية لأن النوع الاستقرائي محفوظ، بينما تتغيّر الشجرة العودية المسجّلة للمعامل. نقطة ثابتة ثانية تستدعي الأولى ترث الشجرة العودية المتغيّرة دون تحقق، لذا يُقبل استدعاء غير متناقص بنيويًا على أنه منتهٍ. التعريف الناتج غير المنتهي يثبت أن عددًا طبيعيًا يساوي خلفه الخاص وبالتالي False، ومنه يستلزم أي قضية. يستخدم البرهان مسلّمتين تتبعان من أحادية القيمة وتتوافقان مع حساب الإنشاءات الاستقرائي، لذا يأتي التناقض من فحص الحماية لا من الافتراضات. اقتُرح إصلاح لكنه لم يُدمج.

المصادر

• rocq-cve-poc-22024PoC

  CVE-2026-72704 — مدقّق Rocq Guard يثق بشجرة تكرارية تالفة بعد النقل