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

मॉड्यूल फ़ंक्टर इनलाइनिंग के माध्यम से प्रमाण ऑडिट को बायपास करना — 2020 से अनसुलझा।

भेद्यता सारांश

Print Assumptions यह रिपोर्ट करने में विफल रहता है कि किसी परिभाषा को यूनिवर्स जाँच अक्षम करके बनाया गया था, जब वह परिभाषा मॉड्यूल प्रकार में Parameter Inline के माध्यम से कॉलर तक पहुँचती है। फ़ंक्टर एप्लिकेशन पैरामीटर के बॉडी को इनलाइन कर देता है और Unset Universe Checking संदर्भ के रिकॉर्ड को हटा देता है, इसलिए परिणामी कॉन्स्टेंट असुरक्षित ऑपरेशन का कोई संकेत नहीं दिखाता।

इसलिए एक मॉड्यूल यूनिवर्स असंगति का उपयोग False को सिद्ध करने के लिए कर सकता है, और Print Assumptions निर्भर प्रमाण को वैश्विक संदर्भ के अंतर्गत बंद (closed) के रूप में रिपोर्ट करता है — कोई स्वयंसिद्ध (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 बंद (closed) के रूप में रिपोर्ट करता है।

प्रभाव

कोई भी वर्कफ़्लो जो Print Assumptions को एकमात्र अखंडता जाँच के रूप में उपयोग करता है, प्रभावित हो सकता है:

• औपचारिक रूप से सत्यापित कंपाइलर (CompCert)
• सत्यापित OS कर्नेल (CertiKOS)
• सेपरेशन लॉजिक फ़्रेमवर्क (Iris)
• गणितीय लाइब्रेरी (MathComp)
• प्रमाण-वाहक कोड (proof-carrying code) जहाँ किसी निर्भरता में एक दुर्भावनापूर्ण .v फ़ाइल अस्वस्थ (unsound) घोषणाएँ पेश कर सकती है जो अनुमान ऑडिटिंग पास कर जाती हैं
• सत्यापित स्मार्ट कॉन्ट्रैक्ट (ConCert)
• कोई भी प्रोजेक्ट जो संकलित आउटपुट पर नियमित रूप से coqchk नहीं चलाता

मूल कारण

जब कोई मॉड्यूल प्रकार Parameter Inline घोषित करता है, तो फ़ंक्टर एप्लिकेशन पैरामीटर के बॉडी को कॉलिंग संदर्भ में इनलाइन कर देता है। यह इनलाइनिंग उस मेटाडेटा को त्याग देती है जो रिकॉर्ड करता है कि मूल परिभाषा Unset Universe Checking के अंतर्गत बनाई गई थी। इसलिए यूनिवर्स ग्राफ़ इनलाइन किए गए बॉडी से असंगत यूनिवर्स बाधाओं को स्वीकार कर लेता है, और Print Assumptions को असुरक्षित संदर्भ का कोई निशान नहीं दिखता।

यह बग 2020 से खुला है (Coq issue #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 — अपर्याप्त लॉगिंग

प्रभावित संस्करण

उत्पाद	प्रभावित	ठीक किया गया
Coq	8.11 – 8.20	अनसुलझा
Rocq Prover	8.20 – 9.2.0	अनसुलझा

शमन

• उत्पादन में प्रमाणों पर भरोसा करने से पहले सभी संकलित .vo फ़ाइलों पर coqchk चलाएँ। coqchk उस यूनिवर्स असंगति को पकड़ लेता है जिसे Print Assumptions चूक जाता है।
• मॉड्यूल निर्भरताओं का ऑडिट करें — हमले के लिए एक ऐसे मॉड्यूल प्रकार की आवश्यकता होती है जिसमें Parameter Inline हो और जिसे Unset Universe Checking के अंतर्गत संकलित किया गया हो।
• Rocq 9.2.0 तक कोई पैच किया गया संस्करण उपलब्ध नहीं है।

संदर्भ

बग रिपोर्ट	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	VulnCheck द्वारा CVE-2020-37268 प्रकाशित
2026-08-24	Docker-पुनरुत्पादनीय PoC प्रकाशित

श्रेय

• बग की खोज: Jason Gross
• PoC पैकेजिंग: Jonathan Brossard (@endrazine) — MOABI / PSIRT.com