CVE-2026-72714

सारांश

Rocq Prover उस मॉड्यूल के बंद होने पर यूनिवर्स ग्राफ़ की यूनिवर्स जाँच फ़्लैग की प्रति को पुनर्स्थापित नहीं करता, जिसने स्थानीय रूप से जाँच को अक्षम किया था। किसी मॉड्यूल के भीतर स्थानीय Unset Universe Checking केवल मॉड्यूल समाप्त होने तक ही टिकना अपेक्षित है, और वैश्विक फ़्लैग पुनर्स्थापित हो जाता है, लेकिन यूनिवर्स ग्राफ़ अपनी अलग प्रति रखता है जो अक्षम ही रह जाती है। तब दोनों दृश्य आपस में असंगत हो जाते हैं: Test Universe Checking जाँच को सक्षम बताता है जबकि कर्नेल यूनिवर्स-असंगत पदों को स्वीकार करता रहता है। दो यूनिवर्सों के बीच के बाध्यता के अब लागू न होने से Hurkens' paradox लागू हो जाता है और False का प्रमाण प्राप्त होता है, जिससे कोई भी प्रस्ताव निकलता है। मॉड्यूल बंद होने के बाद यह प्रमाण किसी भी स्वयंसिद्ध (axiom), प्लगइन या असुरक्षित सुविधा का उपयोग नहीं करता, और Print Assumptions इसे वैश्विक संदर्भ के अंतर्गत बंद (closed) बताता है, इसलिए न तो स्वयंसिद्ध ऑडिट और न ही फ़्लैग क्वेरी वास्तविक कर्नेल स्थिति को दर्शाती है। कोई समाधान उपलब्ध नहीं है।

स्रोत

• rocq-cve-poc-22287PoC

  CVE-2026-72714 — मॉड्यूल बंद होने के बाद Rocq यूनिवर्स चेकिंग स्थिति असमकालिक