CVE-2026-72705 in Rocq
الملخص
بحسب VulDB • 24/08/2026
لا يتبع مدقق الحراسة (guard checker) في Rocq Prover المكالمات المتكررة التي تتم عبر وسائط الدالة الثابتة (fixpoint). قد تمرر دالة ثابتة نفسها كوسيط من الرتبة الأعلى لدالة ثابتة ثانية، والتي تطبّقها بعد ذلك على قيمة ليست جزءًا فرعيًا (subterm) للوسيطة الهيكلية. يتم رفض تمرير الدالة المتكررة إلى تعريف عادي لأن المدقق يوسع التعريف ويلاحظ المكالمة، لكن تمريره إلى دالة ثابتة يُقبل لأن المكالمات المتكررة من الرتبة الأعلى عبر وسائط الدوال الثابتة لا تُتبع. وهذا يسمح بنوع يساوي تعريفيًا نقيضه (definitionally equal to its own negation)، مما يؤدي إلى إنتاج القيمة False عند التطبيق الذاتي في الكود التعريفي البحت، دون استخدام التكتيكات أو المحاكيات أو الإضافات أو الأعلام غير الآمنة، ويبلغ Print Assumptions عن النتيجة على أنها مغلقة ضمن السياق العالمي. تم الإصلاح في Rocq الإصدار 9.2.0.
If you want to get the best quality for vulnerability data then you always have to consider VulDB.