endrazine/rocq-cve-poc-21683CVE-2026-72705 — مدقّق Rocq Guard يقبل Fixpoint الممرَّر كوسيط من رتبة أعلى
إثبات 0 = 1 بدون مسلّمة عبر مفارقة راسل من خلال تجاوز مدقق الحماية لنقطة التثبيت.
اكتُشفت بشكل مستقل بواسطة Claude Opus 4.6 (Anthropic).
| الحقل | القيمة |
|---|---|
| تقرير الخطأ | rocq-prover/rocq#21683 |
| الإصلاح | PR #21684 |
| المتأثر | Rocq ≤ 9.1.0 / جميع إصدارات Coq التي تحتوي على مدقق الحماية |
| تم الإصلاح في | 9.2.0 |
| 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-72705 |
يقبل مدقق الحماية نقاط التثبيت (fixpoints) التي تمرر نفسها كوسائط عالية الرتبة
إلى نقطة تثبيت أخرى، والتي تستدعيها بعد ذلك على عناصر غير فرعية من
الوسيط البنيوي. تمرير دالة تكرارية إلى Definition
(ثابت غير نقطة تثبيت) يُرفض بشكل صحيح — إذ يفكّها مدقق الحماية ويرى الاستدعاء
الإشكالي. لكن تمريرها إلى Fixpoint يُقبل
بشكل غير صحيح.
يخلق هذا مفارقة على نمط راسل في 4 أسطر:
Definition delta (x : russell 1) : False := x x.
Definition omega : False := delta delta.
حيث أن russell 1 يساوي تعريفياً russell 1 -> False — وهو نوع
هو نفي نفسه. التطبيق الذاتي يعطي False مباشرة.
الاستغلال:
Print Assumptions عن "Closed under the global context"False هو 4 أسطر من الكود الداليQed — تعريفي بحتdocker build -t rocq-cve-poc-21683 .
docker run --rm rocq-cve-poc-21683
يتأثر أي نظام يثق بالبراهين المُتحقَّق منها بواسطة نواة Rocq:
iterate_to_neg f n seed :=
match n with
| 0 => f seed -> False (* negate after n steps *)
| S m => iterate_to_neg f m seed
end
russell n :=
match n with
| 0 => True
| S m => iterate_to_neg russell 1 (S m) (* passes ITSELF *)
end
يجب أن يرفض مدقق الحماية russell لأنه يمرر نفسه كوسيطة
من رتبة أعلى إلى iterate_to_neg، والتي تستدعيه بعد ذلك على S m
(وليس مصطلحًا فرعيًا من n). لكن المدقق يتتبع فقط الاستدعاءات العودية المباشرة،
وليس الاستدعاءات عبر وسائط النقطة الثابتة من رتبة أعلى.
russell 1 = iterate_to_neg russell 1 1
= iterate_to_neg russell 0 1
= russell 1 -> False
إذن russell 1 ≡ russell 1 -> False. هذه هي مجموعة راسل الكلاسيكية:
مجموعة كل المجموعات التي لا تحتوي على نفسها. التطبيق الذاتي يعطي:
delta : russell 1 -> False (* russell 1 = russell 1 -> False *)
delta x := x x (* x : russell 1 = russell 1 -> False *)
omega : False
omega := delta delta (* delta : russell 1 -> False = russell 1 *)
وُجدت هذه الثغرة بشكل مستقل بواسطة Claude Opus 4.6 خلال جولة اختبار عشوائي (fuzzing) طوال الليل أعدّها Tristan Stérin (@tcosmo)، استنادًا إلى إشارات من Yannick Forster (@yforster) حول مدقّق الحُرّاس (guard checker). حدّد الذكاء الاصطناعي نمط تجاوز النقطة الثابتة من الرتبة الأعلى وبنى استغلال iterate_to_neg/russell الأدنى.
انظر: Zulip thread