CVE-2026-72705

ملخص

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

المصادر

• rocq-cve-poc-21683PoC

  CVE-2026-72705 — مدقّق Rocq Guard يقبل Fixpoint الممرَّر كوسيط من رتبة أعلى