endrazine/rocq-cve-poc-12155CVE-2020-37268 — يتجاهل Rocq/Coq Print Assumptions فحص الكون غير الآمن عبر Parameter Inline
تجاوز تدقيق البرهان عبر تضمين functor الوحدة — دون إصلاح منذ 2020.
يفشل Print Assumptions في الإبلاغ عن أن تعريفًا ما بُني مع تعطيل فحص الكون (universe checking) عندما يصل ذلك التعريف إلى المستدعي عبر Parameter Inline في نوع وحدة (module type). يؤدي تطبيق functor إلى تضمين جسم المعامل (parameter) وإسقاط السجل الخاص بسياق Unset Universe Checking، لذا لا يُظهر الثابت الناتج أي أثر للعملية غير الآمنة.
وبالتالي يمكن لوحدة ما أن تستخدم عدم اتساق في الكون لإثبات False، ويُبلّغ Print Assumptions عن البرهان التابع على أنه مغلق ضمن السياق العام — دون بديهيات (axioms)، ودون أي أعلام غير آمنة ظاهرة.
يرفض coqchk بالفعل ملف .vo المُجمّع الناتج، لكن تدقيق الافتراضات داخل العملية (Print Assumptions) لا يكتشف المشكلة.
docker build -t rocq-cve-poc-12155 .
docker run --rm rocq-cve-poc-12155
على نسخة مُعرّضة للثغرة (Rocq 8.11 – 9.2.0، وجميع إصدارات Coq 8.x التي تتضمن نظام الوحدات)، يؤكد المخرَج برهان 0 = 1 مع إبلاغ Print Assumptions عنه على أنه مغلق.
قد تتأثر أي سير عمل يعتمد على Print Assumptions كفحص سلامة وحيد:
.v خبيث ضمن تبعية أن يُدخل تصريحات غير سليمة تجتاز تدقيق الافتراضاتcoqchk بانتظام على المخرجات المُجمّعةعندما يعلن نوع وحدة عن Parameter Inline، يقوم تطبيق functor بتضمين جسم المعامل في السياق المستدعي. يتجاهل هذا التضمين البيانات الوصفية التي تسجّل أن التعريف الأصلي أُنتج ضمن Unset Universe Checking. لذلك يقبل رسم الكون (universe graph) قيود كون غير متسقة من الجسم المُضمَّن، ولا يرى Print Assumptions أي أثر للسياق غير الآمن.
الخطأ مفتوح منذ 2020 (قضية Coq رقم #12155) وهو موثّق في dev/doc/critical-bugs.md الخاص بالمشروع. لم يُدمج أي إصلاح حتى إصدار Rocq 9.2.0.
| الحقل | القيمة |
|---|---|
| CVE | CVE-2020-37268 |
| 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-778 — Insufficient Logging |
| المنتج | المتأثر | المُصلَح |
|---|---|---|
| Coq | 8.11 – 8.20 | غير مُصلَح |
| Rocq Prover | 8.20 – 9.2.0 | غير مُصلَح |
coqchk على جميع ملفات .vo المُجمّعة قبل الوثوق بالبراهين في بيئة الإنتاج. يكتشف coqchk عدم الاتساق في الكون الذي يفوته Print Assumptions.Parameter Inline جرى تجميعه ضمن Unset Universe Checking.| تقرير الخطأ | rocq-prover/rocq#12155 |
| وثيقة الأخطاء الحرجة | dev/doc/critical-bugs.md |
| استشارة VulnCheck | vulncheck.com |
| التاريخ | الحدث |
|---|---|
| 2020 | أبلغ Jason Gross عن الخطأ (coq/coq#12155) |
| 2020–2026 | يبقى الخطأ مفتوحًا، وموثّقًا في critical-bugs.md |
| 2026-08-24 | نُشر CVE-2020-37268 بواسطة VulnCheck |
| 2026-08-24 | نُشر PoC قابل لإعادة الإنتاج عبر Docker |