endrazine/rocq-cve-poc-21682CVE-2026-72703 — Rocq Guard Checker अनचेक्ड क्रॉस-कॉल्स के माध्यम से नॉन-टर्मिनेटिंग फिक्सपॉइंट स्वीकार करता है
गार्ड चेकर यूनिफ़ॉर्म पैरामीटर बायपास के माध्यम से 0 = 1 को स्वयंसिद्ध-मुक्त (axiom-free) सिद्ध करना।
Rocq कर्नेल का गार्ड चेकर (फिक्सपॉइंट टर्मिनेशन सत्यापनकर्ता) नेस्टेड म्यूचुअल फिक्सपॉइंट के सभी पैरामीटर को यूनिफ़ॉर्म मानता है, बिना फिक्सपॉइंट के बॉडीज़ के बीच होने वाले कॉल्स की जाँच किए। kernel/inductive.ml में फ़ंक्शन find_uniform_parameters केवल स्व-पुनरावर्ती (self-recursive) कॉल्स का निरीक्षण करता है; जब कोई भी बॉडी स्वयं को कॉल नहीं करती, तो प्रत्येक पैरामीटर को यूनिफ़ॉर्म मान लिया जाता है। क्रॉस-कॉल के माध्यम से बढ़ने वाला पैरामीटर तब एक गलत सबटर्म विनिर्देश बनाए रख सकता है, और एक पुनरावर्ती कॉल स्वीकार कर लिया जाता है, भले ही उसका आर्ग्युमेंट संरचनात्मक रूप से छोटा न हो।
यह एक नॉन-टर्मिनेटिंग परिभाषा को स्वीकार करने की अनुमति देता है जो False को सिद्ध करती है, जिससे कोई भी प्रस्ताव निकलता है — जिसमें 0 = 1 भी शामिल है।
इस प्रमाण के लिए किसी स्वयंसिद्ध (axiom), टैक्टिक, प्लगइन या असुरक्षित फ़्लैग की आवश्यकता नहीं है। Print Assumptions इसे वैश्विक संदर्भ के अंतर्गत बंद (closed) बताता है।
docker build -t rocq-cve-poc-21682 .
docker run --rm rocq-cve-poc-21682
एक भेद्य संस्करण (Rocq 8.20 – <9.2.0) पर, आउटपुट बिना किसी स्वयंसिद्ध के 0 = 1 के प्रमाण की पुष्टि करता है।
एक पैच किए गए संस्करण (Rocq ≥9.2.0) पर, गार्ड चेकर फिक्सपॉइंट को अस्वीकार कर देता है।
कोई भी सिस्टम जो Rocq/Coq कर्नेल-सत्यापित प्रमाणों पर निर्भर करता है, प्रभावित हो सकता है यदि वह बिना अतिरिक्त शमन के किसी भेद्य संस्करण पर चलता है:
.v फ़ाइल अस्वस्थ (unsound) घोषणाएँ पेश कर सकती हैkernel/inductive.ml में find_uniform_parameters म्यूचुअल फिक्सपॉइंट की प्रत्येक बॉडी के भीतर केवल स्व-पुनरावर्ती कॉल्स का निरीक्षण करता है। जब किसी भी बॉडी में स्व-पुनरावर्ती कॉल नहीं होती (सभी कॉल्स बॉडीज़ के बीच क्रॉस-कॉल्स होते हैं), तो प्रत्येक पैरामीटर को यूनिफ़ॉर्म चिह्नित कर दिया जाता है। एक पैरामीटर जो वास्तव में क्रॉस-कॉल्स के दौरान बदलता है, एक गलत सबटर्म विनिर्देश बनाए रखता है, जिससे गार्ड चेकर को गैर-संरचनात्मक रूप से घटते आर्ग्युमेंट पर एक पुनरावर्ती कॉल स्वीकार करने की अनुमति मिल जाती है।
| फ़ील्ड | मान |
|---|---|
| CVE | CVE-2026-72703 |
| 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-670 — Always-Incorrect Control Flow Implementation |
| उत्पाद | प्रभावित | ठीक किया गया |
|---|---|---|
| Rocq Prover | 8.20 – <9.2.0 | 9.2.0 |
.vo फ़ाइलों पर coqchk चलाएँ।| बग रिपोर्ट | rocq-prover/rocq#21682 |
| फ़िक्स | rocq-prover/rocq#21684 |
| VulnCheck सलाह | vulncheck.com |
| तिथि | घटना |
|---|---|
| 2025 | बग की रिपोर्ट की गई (rocq-prover/rocq#21682) |
| 2025 | Rocq 9.2.0 में फ़िक्स मर्ज किया गया (PR #21684) |
| 2026-08-24 | VulnCheck द्वारा CVE-2026-72703 प्रकाशित |
| 2026-08-24 | Docker-पुनरुत्पादनीय PoC प्रकाशित |