CVE-2026-72704 — Rocq गार्ड चेकर ट्रांसपोर्ट के बाद भ्रष्ट पुनरावर्ती ट्री पर भरोसा करता है

गार्ड चेकर फिक्सपॉइंट रेक्ट्री भ्रष्टाचार के माध्यम से सुसंगत स्वयंसिद्धों से 0 = 1 सिद्ध करना।

फ़ील्ड	मान
बग रिपोर्ट	rocq-prover/rocq#22024
फ़िक्स	PR #22027 (खुला)
प्रभावित	Rocq ≤ 9.2.0 / Coq 8.x (गार्ड चेकर वाले सभी संस्करण)
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-670 (सदैव-गलत नियंत्रण प्रवाह कार्यान्वयन)
CVE	CVE-2026-72704

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

Rocq Prover का गार्ड चेकर (फिक्सपॉइंट के लिए टर्मिनेशन चेकर) इंडक्टिव टाइप आर्ग्युमेंट्स के रेक्ट्री प्रतिनिधित्व की पुनः जाँच करने में विफल रहता है जब उन्हें ट्रांसपोर्ट (rew) के माध्यम से संशोधित किया जाता है। एक फिक्सपॉइंट किसी इंडक्टिव के टाइप पैरामीटर के लिए रेक्ट्री को चुपचाप भ्रष्ट कर सकता है, और दूसरा फिक्सपॉइंट जो पहले को कॉल करता है, भ्रष्ट रेक्ट्री पर बिना सत्यापन के भरोसा करेगा, और एक गैर-समाप्त होने वाली परिभाषा को संरचनात्मक रूप से घटती हुई मान लेगा।

यह एक्सप्लॉइट दो स्वयंसिद्धों का उपयोग करता है जो CIC के साथ सुसंगत हैं — वे यूनिवैलेंस स्वयंसिद्ध के प्रत्यक्ष परिणाम हैं (0↔1 की अदला-बदली करने वाला द्विआधारी Type में एक पथ nat = nat देता है जिसके अनुदिश ट्रांसपोर्ट 0 को 1 पर भेजता है)। एक सुदृढ़ गार्ड चेकर को सुसंगत स्वयंसिद्धों से False प्राप्त नहीं करना चाहिए।

यह एक्सप्लॉइट:

केवल दो सुसंगत स्वयंसिद्धों का उपयोग करता है (यूनिवैलेंस के परिणाम)
Print Assumptions केवल उन दो स्वयंसिद्धों की रिपोर्ट करता है — कोई False नहीं, कोई sorry नहीं
कोई प्लगइन, असुरक्षित सुविधाएँ, या यूनिवर्स हेरफेर नहीं
गार्ड चेकर ही असुदृढ़ता का एकमात्र स्रोत है

उपयोग

docker build -t rocq-cve-poc-22024 .
docker run --rm rocq-cve-poc-22024

एक असुरक्षित Rocq संस्करण पर अपेक्षित आउटपुट:

[*] Compiling ZeroEqOne.v with rocq compile ...

zero_eq_one is defined
Axioms:
e : nat = nat
e1 : rew [fun T : Type => T] e in 0 = 1

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Axioms used: e (nat = nat), e1 (transport sends 0 to 1)
    These axioms are consistent (consequences of univalence).
    A sound guard checker must not derive False from them.

    Bug class:  Guard checker rectree corruption (CWE-670)
    Root cause: fixpoints can alter rectrees via transport; nested
                fixpoints trust the corrupted rectree without recheck
    Bug report: https://github.com/rocq-prover/rocq/issues/22024

प्रभाव

कोई भी सिस्टम जो Rocq के kernel-checked प्रमाणों पर और univalence के साथ संगत axioms का उपयोग करता है, प्रभावित है:

HoTT विकास: कोई भी Rocq प्रोजेक्ट जो univalence axiom (या propositional extensionality, जो समान वर्ग के बग को ट्रिगर कर सकता है) का उपयोग करता है, उसके guard-checked fixpoints को non-termination के बावजूद चुपचाप स्वीकार किया जा सकता है।
औपचारिक रूप से सत्यापित सॉफ़्टवेयर: CompCert, CertiKOS, Iris, और कोई भी प्रोजेक्ट जो CIC के साथ संगत कस्टम axioms जोड़ता है, जोखिम में है यदि guard checker ही एकमात्र termination गारंटी है।
Proof-carrying code: एक दुर्भावनापूर्ण dependency दो axioms और भ्रष्ट fixpoint को पेश कर सकता है, फिर downstream में False का उपयोग कर सकता है।

तकनीकी विवरण

Guard Checker बग

Rocq का guard checker यह सत्यापित करता है कि fixpoints संरचनात्मक रूप से घट रहे हैं, एक rectree बनाकर — एक tree जो ट्रैक करता है कि प्रत्येक recursive call पर recursive argument के कौन से subterms उपलब्ध हैं। बग दो-चरणीय विफलता है:

Rectree भ्रष्टाचार: weird Box A पर एक fixpoint है जो wrap case में recursive argument पर rew [Box] e (transport along e : A = A) लागू करता है। Guard checker इसे स्वीकार करता है क्योंकि transport inductive type Box को संरक्षित करता है, लेकिन parameter A के लिए rectree चुपचाप बदल दिया जाता है — transport के बाद, guard checker का आंतरिक मॉडल अब सटीक रूप से ट्रैक नहीं करता कि A के माध्यम से कौन से मान प्रवाहित होते हैं।
अनियंत्रित विश्वास: loop weird loop e (wrap _ (box _ n)) को कॉल करता है। Guard checker loop के अपने recursive calls को सत्यापित करता है लेकिन nested call के लिए weird के rectree पर विश्वास करता है। चूंकि weird का rectree transport द्वारा भ्रष्ट कर दिया गया है, guard checker गलत तरीके से निष्कर्ष निकालता है कि loop संरचनात्मक रूप से घट रहा है।

विरोधाभास

Guard checker को मूर्ख बनाकर, loop को non-terminating होने के बावजूद स्वीकार कर लिया जाता है। प्रमाण फिर दिखाता है:

loop 1 = S (loop 1)

loop और weird को अनफोल्ड करके, और e1 का उपयोग यह दिखाने के लिए करके कि transport box nat 0 को box nat 1 पर भेजता है, जो वापस loop में फीड होता है। चूँकि ∀ n, n ≠ S n आगमन (induction) द्वारा सिद्ध किया जा सकता है, loop 1 = S (loop 1) से False प्राप्त होता है, और उससे 0 = 1।

अभिगृहीत (Axioms) संगत क्यों हैं

दो अभिगृहीत:

e  : nat = nat :> Type
e1 : rew [fun T => T] e in 0 = 1

ये यूनिवैलेंस एक्सिओम के परिणाम हैं। यूनिवैलेंस के अंतर्गत, कोई भी बाइजेक्शन f : nat → nat Type में एक पाथ nat = nat देता है, और उस पाथ के साथ ट्रांसपोर्ट f के रूप में कार्य करता है। बाइजेक्शन swap01 जो 0↦1, 1↦0, और n≥2 के लिए n↦n भेजता है, ऐसा ही एक बाइजेक्शन है, जिसमें swap01 0 = 1 e1 का साक्ष्य देता है।

यूनिवैलेंस को CIC के साथ संगत माना जाता है (क्यूबिकल टाइप थ्योरी मॉडल्स द्वारा सत्यापित)। इसलिए ये एक्सिओम विरोधाभास का स्रोत नहीं हो सकते — गार्ड चेकर है।

अन्य PoC के साथ तुलना

पहलू	Rocq #22024 (यह बग)	Rocq #22287	Lean #14484
बग वर्ग	गार्ड चेकर रेक्ट्री करप्शन	यूनिवर्स चेकिंग स्टेट डीसिंक	इन्फरेंस कैश पॉइज़निंग
आवश्यक एक्सिओम	2 (यूनिवैलेंस के साथ संगत)	कोई नहीं	कोई नहीं
एक्सप्लॉइट जटिलता	~30 पंक्तियाँ	6 पंक्तियाँ	~20 पंक्तियाँ
घटक	गार्ड चेकर (फिक्सपॉइंट)	मॉड्यूल सिस्टम (ugraph फ्लैग)	टाइप चेकर (ओपेक डिक्ल)
फिक्स स्थिति	PR #22027 (खुला)	खुला	फिक्स्ड (PR #14498)

श्रेय

बग की खोज: Yann Leray (@yannl35133)
PoC पैकेजिंग: Jonathan Brossard (@endrazine)

rocq-cve-poc-22024

सबसे लोकप्रिय