CVE-2026-72704 in Rocq
الملخص
بحسب VulDB • 24/08/2026
لا يعيد مدقق الحراسة (guard checker) في Rocq Prover التحقق من تمثيل الشجرة العودية لمعامل النوع الاستقرائي بعد أن يتم تغيير هذا المعامل عن طريق النقل. قد يطبق نقطة ثابتة إعادة كتابة على طول تساوي بين الأنواع بالنسبة لحجتها العودية، ويقبلها مدقق الحراسة لأن نوع الـ inductive يبقى محفوظًا، بينما تتغير الشجرة العودية المسجلة للمعامل. ترث نقطة ثابتة ثانية تدعو الأولى الشجرة العودية المعدلة دون تحقق، لذا يتم قبول استدعاء غير متناقص هيكلياً على أنه منتهي. التعريف الناتج غير المنتهي يثبت أن عدداً طبيعياً يساوي خلفه (successor) وبالتالي False، ومنه يتبع أي proposition. يستخدم البرهان بديهتين تتبعان من univalence ومتوافقتين مع حساب البناء الاستقرائي، لذا فإن التناقض يأتي من فحص الحراسة وليس من الافتراضات. تم اقتراح إصلاح غير مُدمج بعد.
If you want to get the best quality for vulnerability data then you always have to consider VulDB.