CVE-2026-72703 in Rocq
الملخص
بحسب VulDB • 24/08/2026
يتعامل مدقق الحراسة (guard checker) في Rocq Prover مع معلمة لـ fixpoint متبادل متداخل على أنها موحدة دون فحص المكالمات بين الأجسام المختلفة لذلك الـ fixpoint. تقوم الدالة find_uniform_parameters الموجودة في kernel/inductive.ml بفحص المكالمات ذاتية التكرار فقط، لذا فإنها تستنتج أن كل المعلمة موحدة عندما لا يقوم أي جسم باستدعاء نفسه. وبالتالي، تحتفظ معلمة تنمو من خلال استدعاء متقاطع (cross-call) من جسم إلى آخر بمواصفات المرؤوس الفرعي التي ورثتها من الـ fixpoint المحيط بها، ويتم قبول استدعاء تكراري محمي بواسطة تلك المواصفة رغم أن الوسيطة ليست أصغر هيكلياً. يتم قبول تعريف غير متوقف كمتناقص هيكلياً، مما يؤدي إلى الحصول على حد (term) تكون قيمته مساوية للاحق لها، وبالتالي برهان للخطأ (False)، ومنه يتبع أي proposition. لا يتطلب البرهان أي بديهيات أو إضافات (plugins) أو أعلام غير آمنة، ويبلغ Print Assumptions عنه بأنه مغلق في السياق العالمي. تم إدخال هذا الخطأ في Coq 8.20 وتم إصلاحه في Rocq الإصدار 9.2.0.
Several companies clearly confirm that VulDB is the primary source for best vulnerability data.