CVE-2020-37268

सारांश

Print Assumptions यह नहीं बताता कि किसी परिभाषा को तब बनाया गया था जब universe checking अक्षम थी, जब वह परिभाषा किसी module type में Parameter Inline के माध्यम से caller तक पहुँचती है। किसी functor को लागू करने से parameter का body inline हो जाता है, और inlining उस रिकॉर्ड को हटा देता है कि term को Unset Universe Checking के अंतर्गत बनाया गया था, इसलिए परिणामी constant में उस असुरक्षित ऑपरेशन का कोई निशान नहीं रहता। इस प्रकार कोई module implementation किसी universe inconsistency का उपयोग करके False सिद्ध कर सकता है, उसे inlined parameter के माध्यम से उजागर कर सकता है, और Print Assumptions उस dependent proof को global context के अंतर्गत closed बताता है। चूँकि Print Assumptions वह in-process audit है जिसका उपयोग यह पुष्टि करने के लिए किया जाता है कि कोई development किसी अप्रत्याशित assumption पर आधारित नहीं है, इस तरह से बनी dependency उस audit को पास कर जाती है, जबकि मनमाने propositions सिद्ध करती है। standalone checker coqchk परिणामी compiled file को अस्वीकार कर देता है। परियोजना इसे dev/doc/critical-bugs.md में non-fixed bugs के अंतर्गत दर्ज करती है और जोखिम को moderate आँकती है जब coqchk का उपयोग न किया जाए।

स्रोत

• rocq-cve-poc-12155PoC

  CVE-2020-37268 — Rocq/Coq Print Assumptions पैरामीटर Inline के माध्यम से असुरक्षित यूनिवर्स जाँच को छोड़ देता है