CVE-2026-72704 — مدقّق الحماية في Rocq يثق بشجرة تكرارية تالفة بعد النقل

إثبات 0 = 1 من مسلّمات متسقة عبر إفساد الشجرة التكرارية لنقطة ثابتة في مدقّق الحماية.

الحقل	القيمة
تقرير الخطأ	rocq-prover/rocq#22024
الإصلاح	PR #22027 (مفتوح)
المتأثر	Rocq ≤ 9.2.0 / Coq 8.x (جميع الإصدارات التي تحتوي على مدقّق الحماية)
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-670 (تنفيذ تدفق تحكم غير صحيح دائمًا)
CVE	CVE-2026-72704

ملخص الثغرة

يفشل مدقّق الحماية في Rocq Prover (مدقّق الإنهاء لنقاط التثبيت) في إعادة فحص تمثيل الشجرة التكرارية لوسائط النوع الاستقرائي عند تعديلها عبر النقل (rew). يمكن لنقطة تثبيت أن تفسد بصمت الشجرة التكرارية لمعامل نوع استقرائي، ونقطة تثبيت ثانية تستدعي الأولى ستثق بالشجرة التكرارية التالفة دون التحقق منها، فتقبل تعريفًا غير منتهٍ على أنه متناقص بنيويًا.

يستخدم الاستغلال مسلّمتين متسقتين مع CIC — فهما نتيجة مباشرة لمسلّمة التكافؤ (univalence) (التقابل التبادلي الذي يبدّل 0↔1 يعطي مسارًا nat = nat في Type ينقل على طوله 0 إلى 1). يجب ألا يستنتج مدقّق حماية سليم False من مسلّمات متسقة.

الاستغلال:

يستخدم مسلّمتين متسقتين فقط (نتيجتان عن التكافؤ)
يُبلّغ Print Assumptions عن هاتين المسلّمتين فقط — لا False، ولا sorry
لا إضافات (plugins)، ولا ميزات غير آمنة، ولا تلاعب بالأكوان (universes)
مدقّق الحماية هو المصدر الوحيد لعدم السلامة

الاستخدام

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

الناتج المتوقع على إصدار Rocq المصاب:

[*] Compiling ZeroEqOne.v with rocq compile ...

zero_eq_one is defined
Axioms:
e : nat = nat
e1 : rew [fun T : Type => T] e in 0 = 1

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Axioms used: e (nat = nat), e1 (transport sends 0 to 1)
    These axioms are consistent (consequences of univalence).
    A sound guard checker must not derive False from them.

    Bug class:  Guard checker rectree corruption (CWE-670)
    Root cause: fixpoints can alter rectrees via transport; nested
                fixpoints trust the corrupted rectree without recheck
    Bug report: https://github.com/rocq-prover/rocq/issues/22024

التأثير

يتأثر أي نظام يثق ببراهين Rocq المُتحقَّق منها عبر النواة و يستخدم بديهيات متوافقة مع مبدأ أحادية القيمة (univalence):

تطويرات HoTT: أي مشروع Rocq يستخدم بديهية أحادية القيمة (أو الامتدادية القضوية، التي قد تُفعّل نفس فئة الخلل) قد تُقبل نقاط تثبيته الخاضعة لفحص الحارس بصمت رغم عدم انتهائها.
البرمجيات المُتحقَّق منها شكليًا: CompCert وCertiKOS وIris وأي مشروع يضيف بديهيات مخصصة متوافقة مع CIC يكون في خطر إذا كان فاحص الحارس هو الضمان الوحيد للانتهاء.
الشيفرة الحاملة للبرهان: يمكن لتبعية خبيثة أن تُدخل البديهيتين ونقطة التثبيت التالفة، ثم تستخدم False في المصب.

التفاصيل التقنية

خلل فاحص الحارس

يتحقق فاحص الحارس في Rocq من أن نقاط التثبيت تتناقص بنيويًا عبر بناء rectree — وهي شجرة تتعقب أي الحدود الفرعية للوسيط التكراري متاحة عند كل نداء تكراري. الخلل هو فشل من خطوتين:

إفساد الـ rectree: weird هي نقطة تثبيت على Box A تُطبّق rew [Box] e (النقل على طول e : A = A) على الوسيط التكراري في حالة wrap. يقبل فاحص الحارس هذا لأن النقل يحافظ على النوع الاستقرائي Box، لكن الـ rectree الخاص بـ الوسيط A يُعدَّل بصمت — فبعد النقل، لم يعد النموذج الداخلي لفاحص الحارس يتعقب بدقة القيم التي تمر عبر A.
ثقة غير مُتحقَّق منها: يستدعي loop التعبير weird loop e (wrap _ (box _ n)). يتحقق فاحص الحارس من النداءات التكرارية الخاصة بـ loop لكنه يثق بـ rectree الخاص بـ weird للنداء المتداخل. وبما أن rectree الخاص بـ weird قد أُفسد بفعل النقل، يستنتج فاحص الحارس خطأً أن loop تتناقص بنيويًا.

التناقض

بعد خداع فاحص الحارس، تُقبل loop رغم عدم انتهائها. ثم يُظهر البرهان:

loop 1 = S (loop 1)

بفكّ loop وweird، واستخدام e1 لإظهار أن النقل يرسل box nat 0 إلى box nat 1، الذي يعود بدوره إلى loop. بما أن ∀ n, n ≠ S n قابل للإثبات بالاستقراء، فإن loop 1 = S (loop 1) يعطي False، ومنه 0 = 1.

لماذا البديهيات متسقة

البديهيتان:

e  : nat = nat :> Type
e1 : rew [fun T => T] e in 0 = 1

هذه نتائج بديهية التكافؤ (univalence axiom). بموجب التكافؤ، أي تقابل f : nat → nat يعطي مسارًا nat = nat في Type، ويعمل النقل على طول ذلك المسار كما يعمل f. التقابل swap01 الذي يرسل 0↦1، و1↦0، و n↦n من أجل n≥2 هو تقابل من هذا النوع، مع swap01 0 = 1 كشاهد على e1.

من المعروف أن التكافؤ متسق مع CIC (تم التحقق منه بواسطة نماذج نظرية الأنواع المكعبة). لذلك لا يمكن أن تكون هذه البديهيات مصدر التناقض — بل مدقق الحرس (guard checker) هو المصدر.

مقارنة مع إثباتات مفهوم أخرى (PoCs)

الجانب	Rocq #22024 (هذا الخطأ)	Rocq #22287	Lean #14484
فئة الخطأ	تلف شجرة الحرس في مدقق الحرس	عدم تزامن حالة فحص الكون	تسميم ذاكرة التخزين المؤقت للاستدلال
البديهيات المطلوبة	2 (متسقة مع التكافؤ)	لا شيء	لا شيء
تعقيد الاستغلال	~30 سطرًا	6 أسطر	~20 سطرًا
المكوّن	مدقق الحرس (fixpoint)	نظام الوحدات (علامة ugraph)	مدقق الأنواع (تعريف معتم)
حالة الإصلاح	PR #22027 (مفتوح)	مفتوح	تم الإصلاح (PR #14498)

الشكر والتقدير

اكتشاف الخطأ: Yann Leray (@yannl35133)
تجهيز إثبات المفهوم (PoC): Jonathan Brossard (@endrazine)

rocq-cve-poc-22024

الأكثر شعبية