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

إثبات 0 = 1 دون مسلَّمات عبر تجاوز المعاملات الموحَّدة في مدقّق الحماية.

ملخّص الثغرة

يعامل مدقّق الحماية في نواة Rocq (التحقّق من إنهاء النقاط الثابتة) جميع معاملات نقطة ثابتة متبادلة متداخلة كمعاملات موحَّدة دون فحص الاستدعاءات بين أجسام النقطة الثابتة. الدالة find_uniform_parameters في kernel/inductive.ml تفحص فقط الاستدعاءات الذاتية التكرارية؛ وعندما لا يستدعي أي جسم نفسه، يُحكَم على كل معامل بأنه موحَّد. وبالتالي فإن المعامل الذي ينمو عبر استدعاء متقاطع يمكنه الاحتفاظ بمواصفة حدّية فرعية غير صحيحة، ويُقبل الاستدعاء التكراري رغم أن وسيطته ليست أصغر بنيويًا.

يتيح ذلك تعريفًا غير منتهٍ يُثبت False، ومنه تتبع أي قضية — بما في ذلك 0 = 1.

لا يتطلب الإثبات أي مسلَّمات أو تكتيكات أو إضافات أو أعلام غير آمنة. ويُبلّغ Print Assumptions بأنه مغلق في إطار السياق العام.

الاستخدام

docker build -t rocq-cve-poc-21682 .
docker run --rm rocq-cve-poc-21682

على إصدار مُعرَّض للثغرة (Rocq 8.20 – <9.2.0)، يؤكّد المخرَج إثبات 0 = 1 دون أي مسلَّمات.

على إصدار مُرقَّع (Rocq ≥9.2.0)، يرفض مدقّق الحماية النقطة الثابتة.

التأثير

قد يتأثر أي نظام يعتمد على إثباتات مُتحقَّق منها بنواة Rocq/Coq إذا كان يعمل على إصدار مُعرَّض للثغرة دون تخفيف إضافي:

• المترجمات المُتحقَّق منها رسميًا (CompCert)
• أنوية أنظمة التشغيل المُتحقَّق منها (CertiKOS)
• أطر منطق الفصل (Iris)
• المكتبات الرياضية (MathComp)
• الشيفرة الحاملة للإثبات حيث يمكن لملف .v خبيث في أحد التبعيات أن يُدخل تصريحات غير سليمة
• العقود الذكية المُتحقَّق منها (ConCert)

السبب الجذري

تفحص find_uniform_parameters في kernel/inductive.ml فقط الاستدعاءات الذاتية التكرارية داخل كل جسم من أجسام نقطة ثابتة متبادلة. وعندما لا يحتوي أي جسم على استدعاء ذاتي تكراري (جميع الاستدعاءات متقاطعة بين الأجسام)، يُوسم كل معامل بأنه موحَّد. وبالتالي يحتفظ المعامل الذي يتغيّر فعليًا عبر الاستدعاءات المتقاطعة بمواصفة حدّية فرعية غير صحيحة، مما يسمح لمدقّق الحماية بقبول استدعاء تكراري على وسيطة لا تتناقص بنيويًا.

التقييم

الحقل	القيمة
CVE	CVE-2026-72703
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (High)
CVSS 4.0	AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N — 6.8 (Medium)
CWE	CWE-670 — تنفيذ تدفّق تحكّم غير صحيح دائمًا

الإصدارات المتأثرة

المنتج	المتأثر	المُصلَح
Rocq Prover	8.20 – <9.2.0	9.2.0

التخفيف

• الترقية إلى Rocq 9.2.0 أو أحدث.
• تشغيل coqchk على ملفات .vo المُصرَّفة كإجراء دفاعي متعدد الطبقات.

المراجع

تقرير الخطأ	rocq-prover/rocq#21682
الإصلاح	rocq-prover/rocq#21684
استشارة VulnCheck	vulncheck.com

الجدول الزمني

التاريخ	الحدث
2025	الإبلاغ عن الخطأ (rocq-prover/rocq#21682)
2025	دمج الإصلاح (PR #21684) في Rocq 9.2.0
2026-08-24	نشر CVE-2026-72703 بواسطة VulnCheck
2026-08-24	نشر PoC قابل لإعادة الإنتاج عبر Docker

الفضل

• اكتشاف الخطأ: Tristan Stérin، Claude Opus 4.6 (Anthropic)
• إصلاح النواة: PR #21684
• تجهيز PoC: Jonathan Brossard (@endrazine) — MOABI / PSIRT.com