Loading...
श्रृंखला: औपचारिक सत्यापन श्रृंखला · 3 में से भाग 2 पाठकवर्ग: नए पाठक। भाग 1 ने औपचारिक सत्यापन का परिचय दिया था; यहाँ हम उस वास्तविक बग से मिलते हैं जिसने इसे अत्यावश्यक बनाया। आवश्यक हर बात शुरुआत से समझाई गई है। आप क्या समझकर जाएंगे: क्रिप्टोग्राफ़िक प्रमाण प्रणाली में soundness का छेद कैसे हो सकता है, इसका सहज लेकिन सटीक चित्र; 2026 का Zcash "Orchard" बग वास्तव में क्या था; इस प्रकार का बग वर्षों तक क्यों छिप सकता है; और यह पहले भी क्यों हो चुका है।
भाग 1 में हमने कहा था कि परीक्षण बगों की मौजूदगी तो दिखा सकता है, लेकिन उनकी अनुपस्थिति कभी नहीं, और सबसे खतरनाक बग किसी प्रणाली के विनिर्देशन में—उसके अंतर्निहित गणित में—होते हैं। यह लेख उसी का अध्ययन है। 2026 में Zcash के Orchard shielded pool में एक दोष मिला था, जो किसी हमलावर को अदृश्य रूप से असीमित नकली धन बनाने दे सकता था। यह चार वर्ष और बार-बार हुए ऑडिटों तक बचा रहा। इसे और इसके पूर्ववर्तियों को समझना, प्रणालियों को सही सिद्ध करने की सबसे स्पष्ट प्रेरणा है।
Zcash एक निजी मोड वाली क्रिप्टोकरेंसी है। इसके shielded pool में लेनदेन की राशियाँ, प्रेषक और प्राप्तकर्ता छिपे होते हैं। यह गोपनीयता zero-knowledge proofs का उपयोग करके बनाई जाती है: ऐसे क्रिप्टोग्राफ़िक प्रमाण जो लेनदेन की सामग्री बताए बिना सिद्ध करते हैं कि वह सभी नियमों का पालन करता है।
इस डिज़ाइन के दो पहलू हैं। Bitcoin जैसी पारदर्शी लेजर पर, यदि कोई व्यक्ति शून्य से सिक्के पैदा कर दे, तो बढ़ी हुई संख्याएँ सभी को दिखाई देंगी और नेटवर्क उसे पकड़कर वापस कर सकता है। shielded pool में संख्याएँ डिज़ाइन के अनुसार छिपी होती हैं। इसलिए यदि प्रमाण प्रणाली में ही कोई दोष हो, जो अमान्य लेनदेन को वैध दिखा दे, तो जालसाजी पता न लगने योग्य होगी। आप लेजर की जाँच करके इसे नहीं देख सकते, क्योंकि लेजर जानबूझकर अपारदर्शी है।
ठीक यही जोखिम Orchard में वास्तविक हुआ। इसे समझने के लिए हमें देखना होगा कि zero-knowledge proof वास्तव में क्या जाँचता है।
एक सीमा अधिकारी की कल्पना कीजिए, जिसे यात्रियों के दस्तावेज़ सीधे देखे बिना उन्हें मंज़ूरी देनी है। इसके बजाय, हर यात्री एक जाँच-सूची भरता है, और अधिकारी उस व्यक्ति को मंज़ूरी देता है जिसकी सूची पूरी तरह चिन्हित हो। जाँच-सूची इस प्रकार बनाई गई है कि केवल वैध यात्री ही हर खांचे को चिन्हित कर सकता है।
अब मान लीजिए कि जाँच-सूची में एक महत्वपूर्ण खांचा छूट गया है, जैसे, “पासपोर्ट की अवधि समाप्त नहीं हुई है।” लगभग हर व्यक्ति फिर भी इसे ईमानदारी से भरता है और कुछ गलत नहीं दिखता। लेकिन अवधि-समाप्त पासपोर्ट वाला व्यक्ति भी बाकी हर खांचे को चिन्हित कर सकता है और आसानी से निकल सकता है। रोज़मर्रा के उपयोग में प्रणाली ठीक लगती है। यह छेद केवल उसी व्यक्ति के लिए मायने रखता है जो इसे खोजने निकले।
zero-knowledge proof भी उसी जाँच-सूची की तरह काम करता है। यह निजी विवरणों को प्रकट नहीं करता; यह जाँचता है कि वे निश्चित शर्तों के एक समूह को पूरा करते हैं। और यदि कोई आवश्यक शर्त गलती से छूट जाए, तो कुछ अमान्य इनपुट भी पास हो सकते हैं, जबकि सब कुछ सामान्य दिखता रहता है।
आइए “शर्तों की जाँच-सूची” को सटीक बनाते हैं, क्योंकि बग ठीक यहीं था।
अंदरूनी तौर पर, कथन “यह लेनदेन वैध है” को एक सर्किट के रूप में कूटबद्ध किया जाता है: संख्याओं पर समीकरणों के रूप में लिखी गई अंकगणितीय शर्तों का एक निश्चित संग्रह, जिन्हें बाधाएँ कहा जाता है। वैध प्रमाण बनाने के लिए prover को गुप्त मान (जिसे witness कहा जाता है) देने होते हैं, जो हर बाधा को पूरा करते हों। प्रमाण verifier को यह विश्वास दिलाता है कि ऐसा witness मौजूद है, बिना उसे प्रकट किए।
इस प्रणाली से हमें जिस गुण की आवश्यकता है, उसका नाम है:
Soundness: किसी झूठे कथन के लिए वैध प्रमाण बनाना असंभव होना चाहिए। केवल सच्चे कथनों के पास ऐसे witness होने चाहिए जो सभी बाधाओं को पूरा करें।
Soundness जालसाजी-रोधी गारंटी है। यदि soundness बनी रहती है, तो वैध प्रमाण का वास्तव में अर्थ है कि “एक वास्तविक, नियमों का पालन करने वाला लेनदेन हुआ।” यदि soundness में अंतर हो, तो वैध प्रमाण का कोई अर्थ ही नहीं रह सकता।
बाधाओं को अक्सर किसी मान को सरल रखने के लिए बाध्य करना पड़ता है। एक सामान्य उदाहरण: किसी मान b को एकल bit होना बाध्य करना, अर्थात् 0 या 1। ऐसा करने का मानक तरीका एक बाधा है:
b × (b − 1) = 0
यह काम क्यों करता है? गुणनफल तभी शून्य होता है जब उसका कोई एक गुणनखंड शून्य हो। इसलिए b × (b − 1) = 0, b = 0 या b = 1 को बाध्य करता है, और कुछ नहीं। 0 से 16 तक हर मान की जाँच करने पर (उस अंकगणित में जो 17 पर वापस घूमता है), इसे पूरा करने वाले एकमात्र मान ठीक 0 और 1 हैं। ✓
अब कल्पना कीजिए कि वह पंक्ति गलती से सर्किट से छूट जाती है। अचानक b अब बाधित नहीं है। बेईमान prover b को 5, या 9, या कुछ भी रख सकता है, और फिर भी बाकी बाधाओं को पूरा कर सकता है। वह एक छूटी हुई पंक्ति soundness gap है: अब झूठे कथनों के पास संतोषजनक witness हैं।
यह काल्पनिक नहीं है। विकास के दौरान Zcash के पहले shielded डिज़ाइन, Sprout, में बिल्कुल इसी तरह की एक छूटी हुई boolean बाधा मिली थी, और लॉन्च से पहले ठीक कर दी गई थी। Under-constraining इन सर्किटों के निर्माण में सबसे आम और खतरनाक गलतियों में से एक है।
छोटे पैमाने पर यही Orchard बग का पूरा स्वरूप है। अब वास्तविक मामले पर आते हैं।
Zcash के shielded proofs elliptic curves पर बनाए गए हैं, जो गणितीय वस्तुएँ हैं जिनके बिंदुओं को जोड़ा जा सकता है और संख्याओं से “गुणा” किया जा सकता है—ऐसे संचालन जिन्हें सर्किट को बाधाओं द्वारा लागू करना होता है। सर्किट में ऐसे gadgets होते हैं जो elliptic-curve multiplication करते हैं और जाँचते हैं कि वह सही हुआ है।
Shielded Labs और शोधकर्ता Taylor Hornby के प्रकटीकरण के अनुसार, Orchard का दोष ठीक यह था:
Orchard सर्किट का एक अपर्याप्त रूप से बाधित तत्व elliptic-curve multiplication में मनमाने झूठे इनपुट देने और फिर भी multiplication check पास करने की अनुमति देता था।
सरल शब्दों में, सर्किट की जाँच-सूची में वे खांचे नहीं थे जो उस गुणन को निश्चित रूप से निर्धारित करते। इस अंतर के कारण, पर्याप्त विशेषज्ञता वाला हमलावर ऐसा लेनदेन प्रमाण बना सकता था जिसे प्रणाली स्वीकार कर लेती, भले ही लेनदेन ने शून्य से मूल्य बनाया हो। यह जालसाजी है, और क्योंकि shielded pool में राशियाँ छिपी हैं, इसे लेजर से पता नहीं लगाया जा सकता था। Tachyon टीम ने बाद में कोड स्तर पर इसी दोष का वर्णन सर्किट में छूटी हुई पंक्तियों के रूप में किया, जिन्होंने चुपचाप अंतर्निहित समीकरणों को बिगाड़ दिया था।
हमारी जाँच-सूची वाली कहानी से समानताएँ बिल्कुल सटीक हैं:
| जाँच-सूची की कहानी | Orchard बग |
|---|---|
| “पासपोर्ट की अवधि समाप्त नहीं हुई” वाला खांचा छूटा | elliptic-curve multiplication पर एक बाधा छूटी |
| अवधि-समाप्त पासपोर्ट वाला यात्री फिर भी पास हो जाता है | मनमाने झूठे इनपुट multiplication check पास कर जाते हैं |
| बाकी सभी अप्रभावित हैं, इसलिए कुछ गलत नहीं दिखता | सामान्य लेनदेन पूरी तरह काम करते रहे, जिससे दोष छिपा रहा |
| केवल उसे खोजने वाला व्यक्ति ही छेद पाता है | किसी विशेषज्ञ को जानबूझकर सर्किट के गणित को परखना पड़ा |
यह कितना गंभीर था, इसे स्पष्ट करने के लिए: शोधकर्ता ने AI की सहायता से एक पूर्ण कार्यशील exploit लिखा और स्थानीय परीक्षण नेटवर्क में पुष्टि की कि उसने असीमित, पता न लगने योग्य नकली सिक्के उत्पन्न किए। यह वास्तविक और exploit किए जा सकने वाला दोष था, केवल सैद्धांतिक चिंता नहीं।
बग Orchard में मई 2022 में सक्रिय होने से लेकर जून 2026 में आपातकालीन सुधार तक रहा, और दुनिया के कुछ सर्वश्रेष्ठ क्रिप्टोग्राफ़रों द्वारा किए गए बार-बार के पेशेवर ऑडिटों से गुज़रा। कैसे?
क्योंकि, जैसा कि भाग 1 ने चेताया था, परीक्षण मामलों का नमूना लेते हैं, और यह दोष उस मामले में था जिसका किसी ने नमूना नहीं लिया। सामान्य लेनदेन कभी छूटी हुई बाधा तक पहुँचे ही नहीं, इसलिए हर परीक्षण पास हुआ और सामान्य संचालन का प्रत्येक दिन दोषरहित दिखा। यह दोष केवल उस असामान्य witness को जानबूझकर बनाने पर पहुँचा जा सकता था जो सीधे इसी अंतर को लक्ष्य करता हो। अंततः यह परीक्षणों से नहीं, बल्कि सर्किट के गणित पर तर्क करने से मिला।
खोज स्वयं इस बात का संकेत है कि सुरक्षा किस दिशा में जा रही है। अप्रैल 2026 में Shielded Labs ने सुरक्षा शोधकर्ता Taylor Hornby को विशेष रूप से इसी प्रकार के दोष खोजने के लिए नियुक्त किया। मई 2026 के अंत में नए frontier AI मॉडल (Anthropic के Claude Opus 4.8) के जारी होने के तुरंत बाद, Hornby ने एक custom analysis harness और पारंपरिक तरीकों के साथ इसका उपयोग करते हुए Orchard सर्किट की लक्षित समीक्षा की। 29 मई, 2026 को समीक्षा में भेद्यता मिली।
प्रकटीकरण के दो गंभीर तथ्य साफ़-साफ़ कहने योग्य हैं:
Orchard बग एक बार-बार उभरने वाले परिवार से संबंधित है, और उस परिवार को देखना ही औपचारिक सत्यापन को वैकल्पिक नहीं बल्कि अपरिहार्य महसूस कराता है। जालसाजी का दोष हमेशा तीन स्रोतों में से किसी एक तक पहुँचता है (भाग 1 की वर्गीकरण-पद्धति): विनिर्देशन (गणित स्वयं), कार्यान्वयन (सही गणित का पालन न करने वाला कोड), या कोई टूटी हुई धारणा। और महत्वपूर्ण रूप से:
जालसाजी का बग केवल तभी पता न लगने योग्य होता है जब वह विनिर्देशन में हो। कार्यान्वयन बग स्थायी सार्वजनिक साक्ष्य छोड़ते हैं, क्योंकि हर ब्लॉक प्रत्येक लेनदेन की पूरी सामग्री दर्ज करता है, इसलिए सुधारे हुए सॉफ़्टवेयर से इतिहास को पुनः चलाने पर कोई भी ऐसा लेनदेन सामने आ जाएगा जिसे बग वाले कोड ने गलत तरीके से स्वीकार किया था।
Zcash का अपना इतिहास इस पैटर्न को दर्शाता है:
| बग (वर्ष) | स्रोत | पता लगने योग्य? |
|---|---|---|
| Zerocash commitment दोष (2016, लॉन्च-पूर्व) | विनिर्देशन (एक truncated hash ने binding property तोड़ दी) | पता न लगने योग्य |
| Trusted-setup soundness दोष (2018) | विनिर्देशन (अंतर्निहित zk-SNARK पेपर में एक गलती) | पता न लगने योग्य |
| Proving-system query collision (2025) | विनिर्देशन (प्रमाण प्रणाली में छूटी हुई जाँच) | पता लगने योग्य |
| Curve-subgroup validation बग (2016) | कार्यान्वयन (छूटी हुई subgroup जाँच) | पता लगने योग्य |
| Orchard अपर्याप्त रूप से बाधित multiplication (2026) | विनिर्देशन (सर्किट) | पता न लगने योग्य |
संबंध स्पष्ट है: जो दोष हमेशा के लिए छिप सकते हैं, वे गणित में होते हैं। यही वह वर्ग है जिसे विनिर्देशन का machine-checked proof सभी मामलों के लिए एक साथ समाप्त कर सकता है। परीक्षण और ऑडिट नमूने लेते हैं; केवल गणित को सिद्ध करना हर इनपुट को कवर करता है।
Zcash के डेवलपर्स ने तेज़ी से और चरणों में कार्रवाई की:
दूसरा कदम वह स्थान है जहाँ औपचारिक सत्यापन कहानी में प्रवेश करता है, और यही भाग 3 का विषय है। टीम ने जिस समझ पर कार्रवाई की, उसका पूर्वावलोकन करना उचित है, क्योंकि यह पूरी श्रृंखला को जोड़ती है:
एक पता न लगने योग्य जालसाजी दोष केवल प्रोटोकॉल के विनिर्देशन में हो सकता है। इसलिए यदि आप सिद्ध कर सकते हैं कि विनिर्देशन जालसाजी को असंभव बनाता है, तो आप उस पूरे बग-वर्ग को समाप्त कर देते हैं जो यहाँ चार वर्षों तक छिपा रहा।
यही भाग 1 के पहले स्तंभ का विचार है: विनिर्देशन का सत्यापन कीजिए, और उस अंतर को बंद कीजिए जिसे परीक्षण कभी बंद नहीं कर सकता था।
हमने जानबूझकर सरलीकरण किया है। वास्तविक सर्किट में सैकड़ों regions और हजारों बाधाएँ शामिल हैं, और वास्तविक दोष एक छूटी हुई bit-check से अधिक तकनीकी रूप से जटिल है; हमने bit-check का उपयोग इसलिए किया क्योंकि वह अपर्याप्त रूप से बाधित सर्किट का स्वरूप सटीक रूप से दिखाता है, और क्योंकि यही गलती Zcash के इतिहास में वास्तव में हुई थी। जैसा कि आधिकारिक प्रकटीकरण में कहा गया है, सटीक Orchard दोष एक अपर्याप्त रूप से बाधित elliptic-curve multiplication था। हमने प्रकटीकरण और सुधार की समयरेखा भी संक्षिप्त की है। आधिकारिक तकनीकी विवरण के लिए Shielded Labs के प्रकटीकरण और Project Tachyon के लेखों को देखें।
b(b−1)=0, b को 0 या 1 होने के लिए बाध्य करता है; इसे हटाने पर b कुछ भी हो सकता है। इस सटीक बग-वर्ग का उदाहरण Zcash के इतिहास में वास्तविक है।)| शब्द | सरल अर्थ |
|---|---|
| Shielded pool | Zcash का निजी मोड, जहाँ राशियाँ और पक्ष छिपे होते हैं |
| Zero-knowledge proof | ऐसा प्रमाण कि कोई छिपा हुआ कथन वैध है, बिना कुछ और प्रकट किए |
| Circuit | अंकगणितीय शर्तों का निश्चित समूह, जिसे वैध लेनदेन को पूरा करना होता है |
| Constraint | सर्किट के भीतर एक शर्त (समीकरण) |
| Witness | बाधाओं को पूरा करने वाले गुप्त मान |
| Soundness | वह गारंटी कि केवल सच्चे कथन ही वैध प्रमाण उत्पन्न कर सकते हैं |
| Soundness gap | छूटी हुई बाधा जो झूठे कथनों को पास होने देती है |
| Under-constrained | ऐसा सर्किट जिसमें आवश्यक शर्त छूट गई हो, Orchard बग का मूल कारण |
| Detectable / undetectable | क्या exploit सार्वजनिक लेजर में साक्ष्य छोड़ेगा या नहीं |
क्या वास्तव में नकली Zcash बनाए गए थे?
Exploit होने का कोई प्रमाण नहीं मिला, और टीम इसे असंभावित मानती है। लेकिन क्योंकि लेजर से इस दोष का पता नहीं चल सकता था, केवल लेजर से पूरी तरह सिद्ध नहीं किया जा सकता कि यह कभी हुआ ही नहीं, इसलिए प्रतिक्रिया इतनी व्यापक थी।
राशियाँ छिपाने से बग अधिक गंभीर क्यों हो जाता है?
पारदर्शी chain पर बनाए गए सिक्के दिखाई देते हैं और पकड़े तथा वापस किए जा सकते हैं। गोपनीयता के लिए राशियाँ छिपाए जाने पर, जालसाजी बग कोई दृश्यमान असामान्यता उत्पन्न नहीं करता, इसलिए वह अनदेखा बना रह सकता है।
वर्षों के ऑडिट इसे क्यों नहीं पकड़ पाए?
ऑडिट और परीक्षण मुख्यतः यथार्थवादी मामलों में व्यवहार देखते हैं। यह दोष केवल गणितीय edge case को लक्षित करने वाले जानबूझकर बनाए गए, असामान्य इनपुट पर उभरता था, जिसे नियमित समीक्षा ने उपयोग नहीं किया। यह परीक्षण से नहीं, बल्कि सर्किट पर लक्षित तर्क से मिला।
क्या केवल एक छूटी हुई बाधा ही पर्याप्त है?
हाँ। प्रमाण प्रणाली अपने बाधाओं के पूर्ण समूह जितनी ही मजबूत होती है। एक आवश्यक शर्त का छूट जाना अमान्य कथनों को भीतर आने देने के लिए पर्याप्त है।
AI की क्या भूमिका थी?
एक शोधकर्ता ने सर्किट के गणित की समीक्षा और दोष खोजने के लिए frontier AI मॉडल का उपयोग एक custom harness और पारंपरिक तरीकों के साथ किया। AI का उपयोग सुरक्षा के दोनों पक्षों में बढ़ रहा है, जो इस बात का हिस्सा है कि अब प्रणालियों को सही सिद्ध करना इतना महत्वपूर्ण क्यों है।
मान लीजिए किसी shielded लेनदेन को सिद्ध करना है कि “अंदर आने वाला धन बाहर जाने वाले धन के बराबर है,” लेकिन सर्किट एक output value को बाधित करना भूल जाता है। बेईमान prover क्या कर सकता है, और सार्वजनिक लेजर बिल्कुल सामान्य क्यों दिखेगा? (उत्तर नीचे है।)
उस output के बाधित न होने पर, prover उसे वास्तविक inputs से संभव राशि से अधिक रख सकता है, और शून्य से मूल्य बना सकता है—एक नकली धनराशि। प्रमाण फिर भी सत्यापित हो जाएगा, क्योंकि छूटी हुई बाधा ही एकमात्र चीज़ है जो असंतुलन पकड़ती। और चूँकि shielded pool राशियाँ छिपाता है, लेजर केवल यह दिखाता है कि “एक वैध लेनदेन हुआ,” जिसमें चेतावनी देने वाला कोई दृश्यमान असंतुलन नहीं होता। जालसाजी वास्तविक है लेकिन अदृश्य, और यही कारण है कि सर्किट की soundness इतनी महत्वपूर्ण है तथा उसे परीक्षण के बजाय सिद्ध किया जाना चाहिए।
भाग 3 · Ironwood: सुधार केवल एक patch नहीं था। Zcash के इंजीनियरों ने एक नया shielded pool बनाया और उसके साथ Lean proof assistant में लिखे गए 2,700 से अधिक प्रमेयों का एक machine-checked गणितीय प्रमाण दिया कि वह अपनी बताई गई धारणाओं के अंतर्गत नकली धन नहीं बना सकता। हम देखेंगे कि “balance integrity” और “knowledge soundness” का क्या अर्थ है, प्रमाण वास्तव में क्या कवर करता है और क्या नहीं, तथा पुराने pool को सुरक्षित रूप से कैसे हटाया गया।
ZecHub के लिए Formal Verification श्रृंखला का हिस्सा।