CVE-2026-72703

ملخص

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

المصادر

• rocq-cve-poc-21682PoC

  CVE-2026-72703 — يقبل مدقق Rocq Guard نقطة تثبيت غير منتهية عبر استدعاءات متقاطعة غير مُتحقَّق منها