CVE-2020-37268

ملخص

لا يُبلّغ Print Assumptions عن أن تعريفًا أُنتج أثناء تعطيل فحص الكون (universe checking) عندما يصل ذلك التعريف إلى المستدعي عبر Parameter Inline في نوع وحدة (module type). فتطبيق functor يُضمّن جسم المعامل (parameter)، ويُسقط التضمين السجل الذي يفيد بأن المصطلح بُني تحت Unset Universe Checking، وبالتالي لا يحمل الثابت الناتج أي أثر للعملية غير الآمنة. وبناءً على ذلك، يمكن لتنفيذ وحدة (module implementation) أن يُثبت False باستخدام تناقض في الكون، ويكشفه عبر معامل مُضمَّن، ويجعل Print Assumptions يُبلّغ عن البرهان التابع على أنه مغلق في إطار السياق العام (global context). ولأن Print Assumptions هو التدقيق داخل العملية (in-process) المستخدم للتأكد من أن تطويرًا ما لا يعتمد على أي افتراضات غير متوقعة، فإن اعتمادية مبنية بهذه الطريقة تجتاز ذلك التدقيق بينما تُثبت قضايا اعتباطية. أما المدقق المستقل coqchk فيرفض الملف المُصرَّف الناتج. ويسجّل المشروع ذلك في dev/doc/critical-bugs.md ضمن الأخطاء غير المُصلحة، ويُصنّف الخطر بأنه متوسط عندما لا يُستخدم coqchk.

المصادر

• rocq-cve-poc-12155PoC

  CVE-2020-37268 — يتجاهل Rocq/Coq Print Assumptions فحص الكون غير الآمن عبر Parameter Inline