CVE-2026-72714 — إلغاء تزامن حالة فحص الأكوان في Rocq بعد إغلاق الوحدة

إثبات 0 = 1 دون مسلَّمات عبر إلغاء تزامن علم فحص الأكوان على مستوى الوحدة.

الحقل	القيمة
تقرير الخطأ	rocq-prover/rocq#22287
الإصلاح	لا يوجد (المشكلة مفتوحة حتى 2026-08-16)
المتأثر	Rocq ≤ 9.2.0 / Coq 8.x (جميع الإصدارات التي تتضمن Hurkens في stdlib)
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-488 (Exposure of Data Element to Wrong Session)، CWE-20 (Improper Input Validation)
CVE	CVE-2026-72714

ملخص الثغرة

يفشل نظام الوحدات في Rocq Prover في تحديد نطاق علم Local Unset Universe Checking بشكل صحيح. عند استخدامه داخل وحدة، ينبغي استعادة العلم إلى حالته السابقة عند إغلاق الوحدة. ومع ذلك، يحتفظ مخطط الأكوان (ugraph) بنسخته الخاصة من العلم، والتي تصبح غير متزامنة مع الحالة العامة عند إغلاق الوحدة.

بعد إلغاء التزامن:

يُبلِّغ Test Universe Checking عن الحالة مفعّلة (تمت استعادة العلم العام)
لا يزال ugraph يحتفظ بفحص الأكوان معطّلًا (لم تتم استعادة نسخته)
لذلك يقبل النواة (kernel) حدودًا غير متسقة مع الأكوان دون خطأ

مع تعطيل فحص الأكوان فعليًا، تنطبق مفارقة Hurkens: يستغل TypeNeqSmallType.paradox حقيقة أنه يمكن الخلط بين Type@{u} و Type@{v} حيث u < v عندما لا تُفرَض قيود الأكوان، مما يُنتج برهانًا مباشرًا على False.

الاستغلال:

لا يستخدم أي مسلَّمات أو إضافات (plugins) أو ميزات غير آمنة
يُبلِّغ Print Assumptions عن "Closed under the global context"
يتطلب فقط Stdlib.Logic.Hurkens (جزء من المكتبة القياسية)
يتكوّن من 6 أسطر من شيفرة البرهان

الاستخدام

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

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

[*] Compiling ZeroEqOne.v ...
Universe Checking is on.
bad is defined
Closed under the global context
zero_eq_one is defined
Closed under the global context

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Depends on: no axioms (closed under the global context)

    Bug class:  Universe checking state desync (CWE-488)
    Root cause: ugraph retains stale Local Unset Universe Checking flag
    Bug report: https://github.com/rocq-prover/rocq/issues/22287

التأثير

يتأثر أي نظام يثق بالبراهين المُتحقَّق منها عبر نواة Rocq:

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

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

السبب الجذري

يحتوي رسم الكون (ugraph) في النواة على نسخته الخاصة من علامة Universe Checking. عندما تستخدم وحدة ما Local Unset Universe Checking، تُعدَّل العلامة في كلٍّ من الحالة العامة وugraph. وعند إغلاق الوحدة، تُستعاد الحالة العامة من الحالة المحفوظة للوحدة، لكن نسخة ugraph لا تُزامَن، مما يترك التحقق من الكون معطَّلًا فعليًا.

مسار الهجوم

┌─────────────────────────────────────────────────────┐
│ 1. Universes u v.  Constraint u < v.                │
│    → Declare universes with strict ordering          │
├─────────────────────────────────────────────────────┤
│ 2. Module Off.                                       │
│      Local Unset Universe Checking.                  │
│    End Off.                                          │
│    → ugraph flag stays OFF after module closes        │
├─────────────────────────────────────────────────────┤
│ 3. Test Universe Checking.  → reports "on" (LIE)     │
├─────────────────────────────────────────────────────┤
│ 4. eapply TypeNeqSmallType.paradox; reflexivity.     │
│    → Kernel accepts universe-inconsistent proof       │
│    → False proved with no axioms                     │
├─────────────────────────────────────────────────────┤
│ 5. zero_eq_one : 0 = 1                              │
│    → Derived via exfalso                             │
└─────────────────────────────────────────────────────┘

مقارنة مع أخطاء نواة Lean 4

الجانب	Rocq #22287 (هذا الخطأ)	Lean #14484	Lean #14576
مساعد الإثبات	Rocq (Coq)	Lean 4	Lean 4
فئة الخطأ	عدم تزامن الحالة في نظام الوحدات	تسميم ذاكرة التخزين المؤقت للاستدلال	خلط الأنواع عبر الإسقاطات
تعقيد الاستغلال	6 أسطر	~20 سطرًا	~50 سطرًا
نظام الأكوان/الأنواع	تجاوز فحص الأكوان	قبول Opaque FVar	هروب المعاملات الوهمية
حالة الإصلاح	مفتوح	مُصلح (PR #14498)	مُصلح (PR #14577)

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

اكتشاف الخطأ: Gaëtan Gilbert (@SkySkimmer)
تجهيز PoC: Jonathan Brossard (@endrazine)

rocq-cve-poc-22287

الأكثر شعبية