CVE-2026-72705 — Rocq गार्ड चेकर उच्च-क्रम तर्क के रूप में पारित Fixpoint को स्वीकार करता है

गार्ड चेकर fixpoint बायपास के माध्यम से रसेल के विरोधाभास द्वारा 0 = 1 को स्वयंसिद्ध-मुक्त सिद्ध करना।

Claude Opus 4.6 (Anthropic) द्वारा स्वायत्त रूप से खोजा गया।

फ़ील्ड	मान
बग रिपोर्ट	rocq-prover/rocq#21683
फ़िक्स	PR #21684
प्रभावित	Rocq ≤ 9.1.0 / गार्ड चेकर वाले सभी Coq संस्करण
में ठीक किया गया	9.2.0
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-72705

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

गार्ड चेकर ऐसे fixpoints को स्वीकार करता है जो स्वयं को उच्च-क्रम तर्कों के रूप में किसी अन्य fixpoint को पारित करते हैं, जो फिर उन्हें संरचनात्मक तर्क के गैर-उपपदों पर कॉल करता है। किसी Definition (गैर-fixpoint स्थिरांक) को पुनरावर्ती फ़ंक्शन पारित करना सही ढंग से अस्वीकार किया जाता है — गार्ड चेकर इसे अनफ़ोल्ड करता है और समस्याग्रस्त कॉल देखता है। लेकिन इसे किसी Fixpoint को पारित करना गलत तरीके से स्वीकार कर लिया जाता है।

यह 4 पंक्तियों में रसेल-शैली का विरोधाभास उत्पन्न करता है:

Definition delta (x : russell 1) : False := x x.
Definition omega : False := delta delta.

जहाँ russell 1 परिभाषा के अनुसार russell 1 -> False के बराबर है — एक प्रकार जो स्वयं का निषेध है। स्व-अनुप्रयोग सीधे False देता है।

एक्सप्लॉइट:

कोई स्वयंसिद्ध (axioms), प्लगइन, या असुरक्षित सुविधाओं का उपयोग नहीं करता
Print Assumptions रिपोर्ट करता है "Closed under the global context"
False का संपूर्ण प्रमाण फंक्शनल कोड की 4 पंक्तियाँ हैं
कोई टैक्टिक्स नहीं, कोई Qed नहीं — पूर्णतः परिभाषात्मक

उपयोग

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

प्रभाव

कोई भी सिस्टम जो Rocq के kernel-checked proofs पर भरोसा करता है, प्रभावित है:

औपचारिक रूप से सत्यापित सॉफ़्टवेयर: CompCert, CertiKOS, Iris, MathComp
स्मार्ट कॉन्ट्रैक्ट्स: ConCert, सत्यापित DeFi
AI-जनित प्रमाण: कोई भी सिस्टम जो Rocq को विश्वसनीय बैकएंड के रूप में उपयोग करता है

तकनीकी विवरण

विरोधाभास निर्माण

iterate_to_neg f n seed :=
  match n with
  | 0   => f seed -> False      (* negate after n steps *)
  | S m => iterate_to_neg f m seed
  end

russell n :=
  match n with
  | 0   => True
  | S m => iterate_to_neg russell 1 (S m)   (* passes ITSELF *)
  end

गार्ड चेकर को russell को अस्वीकार करना चाहिए क्योंकि यह स्वयं को iterate_to_neg के लिए उच्च-क्रम तर्क के रूप में पास करता है, जो फिर इसे S m पर कॉल करता है (n का उपपद नहीं)। लेकिन चेकर केवल प्रत्यक्ष पुनरावर्ती कॉलों को ट्रैक करता है, उच्च-क्रम फिक्सपॉइंट तर्कों के माध्यम से कॉलों को नहीं।

न्यूनीकरण

russell 1 = iterate_to_neg russell 1 1
          = iterate_to_neg russell 0 1
          = russell 1 -> False

तो russell 1 ≡ russell 1 -> False। यह क्लासिकल रसेल समुच्चय है: उन सभी समुच्चयों का समुच्चय जो स्वयं को नहीं रखते। स्व-अनुप्रयोग देता है:

delta : russell 1 -> False    (* russell 1 = russell 1 -> False *)
delta x := x x                (* x : russell 1 = russell 1 -> False *)

omega : False
omega := delta delta           (* delta : russell 1 -> False = russell 1 *)

खोज

यह बग Claude Opus 4.6 द्वारा Tristan Stérin (@tcosmo) द्वारा सेट किए गए एक रात्रिकालीन फ़ज़िंग रन के दौरान स्वायत्त रूप से पाया गया था, जो Yannick Forster (@yforster) के guard checker पर दिए गए संकेतों पर आधारित था। AI ने higher-order fixpoint bypass पैटर्न की पहचान की और न्यूनतम iterate_to_neg/russell exploit का निर्माण किया।

देखें: Zulip thread

श्रेय

बग की खोज: Claude Opus 4.6 (Anthropic), सेटअप Tristan Stérin (@tcosmo) द्वारा
Kernel fix: PR #21684
PoC पैकेजिंग: Jonathan Brossard (@endrazine)

rocq-cve-poc-21683

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