endrazine/rocq-cve-poc-22287CVE-2026-72714 — मॉड्यूल बंद होने के बाद Rocq यूनिवर्स चेकिंग स्थिति असमकालिक
मॉड्यूल-स्कोप्ड यूनिवर्स चेकिंग फ्लैग डीसिंक्रोनाइज़ेशन के माध्यम से बिना किसी स्वयंसिद्ध (axiom) के 0 = 1 सिद्ध करना।
| फ़ील्ड | मान |
|---|---|
| बग रिपोर्ट | rocq-prover/rocq#22287 |
| फ़िक्स | कोई नहीं (2026-08-16 तक इश्यू खुला है) |
| प्रभावित | Rocq ≤ 9.2.0 / Coq 8.x (stdlib में Hurkens वाले सभी संस्करण) |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 |
| CWE | CWE-488 (Exposure of Data Element to Wrong Session), CWE-20 (Improper Input Validation) |
| CVE | CVE-2026-72714 |
Rocq Prover का मॉड्यूल सिस्टम Local Unset Universe Checking फ्लैग को
ठीक से स्कोप करने में विफल रहता है। जब किसी मॉड्यूल के अंदर उपयोग किया जाता है, तो
मॉड्यूल बंद होने पर फ्लैग को उसकी पिछली स्थिति में बहाल किया जाना चाहिए। हालाँकि,
यूनिवर्स ग्राफ़ (ugraph) फ्लैग की अपनी एक प्रति रखता है, जो मॉड्यूल बंद होने पर
वैश्विक स्थिति के साथ सिंक से बाहर हो जाती है।
डीसिंक के बाद:
Test Universe Checking on रिपोर्ट करता है (वैश्विक फ्लैग बहाल हो गया था)ugraph में अभी भी यूनिवर्स चेकिंग off है (इसकी प्रति बहाल नहीं हुई)यूनिवर्स चेकिंग के प्रभावी रूप से अक्षम होने के साथ, Hurkens का विरोधाभास लागू होता है:
TypeNeqSmallType.paradox इस तथ्य का फ़ायदा उठाता है कि जब यूनिवर्स बाधाएँ
लागू नहीं होतीं, तो u < v वाले Type@{u} और Type@{v} को आपस में
भ्रमित किया जा सकता है, जिससे False का सीधा प्रमाण प्राप्त होता है।
एक्सप्लॉइट:
Print Assumptions "Closed under the global context" रिपोर्ट करता हैStdlib.Logic.Hurkens की आवश्यकता होती है (जो मानक लाइब्रेरी का हिस्सा है)docker build -t rocq-cve-poc-22287 .
docker run --rm rocq-cve-poc-22287
एक असुरक्षित Rocq संस्करण पर अपेक्षित आउटपुट:
[*] Compiling ZeroEqOne.v ...
Universe Checking is on.
bad is defined
Closed under the global context
zero_eq_one is defined
Closed under the global context
[!] VULNERABILITY CONFIRMED
zero_eq_one : 0 = 1
Depends on: no axioms (closed under the global context)
Bug class: Universe checking state desync (CWE-488)
Root cause: ugraph retains stale Local Unset Universe Checking flag
Bug report: https://github.com/rocq-prover/rocq/issues/22287
कोई भी सिस्टम जो Rocq के kernel-checked proofs पर भरोसा करता है, प्रभावित होता है:
.v फ़ाइल चुपचाप
अस्वस्थ घोषणाएँ (unsound declarations) पेश कर सकती है जिन पर downstream proofs निर्भर करते हैं।kernel में universe graph (ugraph) में Universe Checking flag की अपनी
प्रति होती है। जब कोई module Local Unset Universe Checking का उपयोग करता है,
तो flag वैश्विक स्थिति (global state) और ugraph दोनों में संशोधित होता है। जब
module बंद होता है, तो वैश्विक स्थिति module की सहेजी गई स्थिति से पुनर्स्थापित होती है,
लेकिन ugraph की प्रति समन्वयित (synchronized) नहीं होती, जिससे universe checking
प्रभावी रूप से अक्षम रह जाती है।
┌─────────────────────────────────────────────────────┐
│ 1. Universes u v. Constraint u < v. │
│ → Declare universes with strict ordering │
├─────────────────────────────────────────────────────┤
│ 2. Module Off. │
│ Local Unset Universe Checking. │
│ End Off. │
│ → ugraph flag stays OFF after module closes │
├─────────────────────────────────────────────────────┤
│ 3. Test Universe Checking. → reports "on" (LIE) │
├─────────────────────────────────────────────────────┤
│ 4. eapply TypeNeqSmallType.paradox; reflexivity. │
│ → Kernel accepts universe-inconsistent proof │
│ → False proved with no axioms │
├─────────────────────────────────────────────────────┤
│ 5. zero_eq_one : 0 = 1 │
│ → Derived via exfalso │
└─────────────────────────────────────────────────────┘
| पहलू | Rocq #22287 (यह बग) | Lean #14484 | Lean #14576 |
|---|---|---|---|
| प्रूफ असिस्टेंट | Rocq (Coq) | Lean 4 | Lean 4 |
| बग वर्ग | मॉड्यूल सिस्टम में स्टेट डीसिंक | इन्फरेंस कैश पॉइज़निंग | प्रोजेक्शन के माध्यम से टाइप कन्फ्यूज़न |
| एक्सप्लॉइट जटिलता | 6 पंक्तियाँ | ~20 पंक्तियाँ | ~50 पंक्तियाँ |
| यूनिवर्स/टाइप सिस्टम | यूनिवर्स चेकिंग बायपास | अपारदर्शी FVar स्वीकृत | फैंटम पैरामीटर एस्केप |
| फ़िक्स स्थिति | खुला | फ़िक्स्ड (PR #14498) | फ़िक्स्ड (PR #14577) |