औपचारिक सत्यापन गणितीय रूप से यह साबित करने की प्रक्रिया है कि कोई प्रोग्राम किसी स्पेसिफिकेशन (specification) का पालन करता है।

यह लेख वैचारिक रूप से प्रस्तुत करता है कि औपचारिक सत्यापन कैसे काम करता है, इसकी फ़ज़िंग (fuzzing) से तुलना कैसे की जाती है, और औपचारिक सत्यापन की सीमाएँ और लाभ क्या हैं।

“Specification” की परिभाषा

स्पेसिफिकेशन विशिष्ट परिस्थितियों में एक अच्छी तरह से परिभाषित व्यवहार (well-defined behavior) होता है।

यहाँ स्पेसिफिकेशन के कुछ उदाहरण दिए गए हैं जो DeFi स्मार्ट कॉन्ट्रैक्ट्स पर लागू होते हैं:

(1) यदि कोई समय नहीं बीता है तो ऋणदाताओं (lenders) को कोई ब्याज नहीं मिलना चाहिए।

(2) यदि समय बीत चुका है, और सक्रिय उधार (active borrows) हैं, तो ऋणदाता को शून्य से अधिक ब्याज मिलना चाहिए।

(3) यदि प्रोटोकॉल रुका (paused) नहीं है, तो उधारकर्ता (borrowers) हमेशा अपना ऋण चुका सकते हैं।

(4) यदि सप्लाई कैप पार नहीं हुई है और प्रोटोकॉल रुका नहीं है, तो ऋणदाता हमेशा डिपॉजिट कर सकते हैं।

औपचारिक सत्यापन हमें किसी कॉन्ट्रैक्ट की आंतरिक स्थिति (internal state) के बारे में तर्क करने की भी अनुमति देता है। हम निम्नलिखित जैसे स्पेसिफिकेशन्स लिख सकते हैं जो पूरी तरह से स्टोरेज वेरिएबल्स का निरीक्षण करते हैं:

(5) लेनदेन के किसी भी क्रम के लिए, ERC-20 टोकन के बैलेंस का योग कुल सप्लाई के बराबर होना चाहिए।

(6) यदि deposit() को कॉल नहीं किया जाता है, तो balance नहीं बढ़ सकता है।

मान लीजिए कि हमारे पास यह निश्चित रूप से जानने का एक तरीका है कि “(1) यदि कोई समय नहीं बीता है तो ऋणदाताओं को कोई ब्याज नहीं मिलना चाहिए।” उस मामले में, हम जानते हैं कि ऐसे ब्याज के माध्यम से प्रोटोकॉल से पैसा चुराने का वह विशेष अटैक वेक्टर जो अर्जित नहीं किया जाना चाहिए, असंभव है। हालांकि हम यह गारंटी नहीं देते कि प्रोटोकॉल में कोई बग नहीं है, हम जानते हैं कि इसमें कोई विशेष बग नहीं है।

यदि स्पेसिफिकेशन “(2) यदि समय बीत चुका है, और सक्रिय उधार हैं, तो ऋणदाता को शून्य से अधिक ब्याज मिलना चाहिए” का उल्लंघन होता है, तो इसके प्रभावों पर विचार करें। इसका मतलब है कि कोई पैसा उधार ले रहा है, लेकिन ऋणदाता ब्याज नहीं कमा रहा है। इसका मतलब है कि या तो:

• एक बग है जहाँ प्रोटोकॉल ब्याज कमा रहा है, लेकिन ऋणदाता नहीं
• उधारकर्ता ऐसा ब्याज दे रहा है जो किसी ऐसे अकाउंट में जा रहा है जहाँ उसे नहीं जाना चाहिए — या ब्याज बर्न (burn) हो रहा है
• उधारकर्ता कोई ब्याज नहीं दे रहा है

निश्चित रूप से यह जानने की अच्छी बात यह है कि स्पेसिफिकेशन 2 लागू होता है, इससे हम यह जानते हैं कि उपरोक्त में से कोई भी बग प्रोटोकॉल पर लागू नहीं होता है।

यदि 3 और 4 लागू होते हैं, तो यह डिनायल-ऑफ-सर्विस (denial-of-service) हमलों की पूरी श्रेणियों को समाप्त कर देता है। यदि किसी हमलावर के पास उधारकर्ताओं को चुकाने से रोकने का कोई तरीका होता, तो वे उधारकर्ताओं को ब्याज बढ़ाने के लिए मजबूर कर सकते थे और फिर अनुचित लाभ के लिए उधारकर्ताओं को लिक्विडेट (liquidate) कर सकते थे। इसके विपरीत, यदि हमलावर ऋणदाताओं को डिपॉजिट करने से रोक सकते हैं, तो एक दुर्भावनापूर्ण प्रतिस्पर्धी शुरुआत में ही डिपॉजिट्स को रोककर उस प्रोटोकॉल से लिक्विडिटी (liquidity) को दूर ले जाने का प्रयास कर सकता है।

यदि 5 और 6 लागू होते हैं, तो हम सुनिश्चित हो सकते हैं कि ERC-20 स्टोरेज वेरिएबल्स के बेमेल अकाउंटिंग से संबंधित कोई बग नहीं हैं।

औपचारिक सत्यापन केवल उन्हीं बग्स को पकड़ सकता है जिनके लिए हम कोई स्पेसिफिकेशन बनाते हैं। ERC-20 उदाहरण का उपयोग करते हुए, यदि हम burn(address from, uint256 amount) फ़ंक्शन को असुरक्षित छोड़ देते हैं (यानी हम किसी को भी इसे कॉल करने देते हैं — इसमें कोई एक्सेस कंट्रोल नहीं है), तो उपरोक्त में से कोई भी स्पेसिफिकेशन इस गायब एक्सेस कंट्रोल को नहीं पकड़ पाएगा।

औपचारिक सत्यापन टूल जिसका हम इस श्रृंखला में अध्ययन करेंगे, Certora Prover, बाइटकोड स्तर पर स्मार्ट कॉन्ट्रैक्ट्स के बारे में तर्क करता है। इसका अर्थ यह है कि यदि कंपाइलर द्वारा कोई बग प्रस्तुत किया जाता है, तो औपचारिक सत्यापन उसे पकड़ सकता है, जब तक कि उस बग के परिणामस्वरूप हमारे किसी स्पेसिफिकेशन का उल्लंघन होता है।

स्टेट ट्रांज़िशन (state transitions) के बारे में एक कथन के रूप में स्पेसिफिकेशन

“किसी ERC-20 टोकन के सभी बैलेंस का योग कुल सप्लाई के बराबर होना चाहिए” स्पेसिफिकेशन का उपयोग करते हुए, औपचारिक सत्यापन टूल दो चीजों को परिभाषित करेगा:

1. एक स्टेट ट्रांज़िशन फ़ंक्शन $\phi$
2. स्टेट का प्रतिनिधित्व (किसी निश्चित समय पर मानों का संग्रह, जैसे किसी कॉन्ट्रैक्ट के स्टेट वेरिएबल्स और Ethereum अकाउंट बैलेंस), जिसे हम केवल $\texttt{state}$ कहते हैं। हम किसी विशेष स्टेट को $\texttt{state}_i$ और एक अलग स्टेट को $\texttt{state}_j$ कह सकते हैं। हम $\texttt{state}_{i+1}$ का भी उल्लेख कर सकते हैं जो उस लेनदेन के बाद की स्टेट है जो $\texttt{state}_i$ के दौरान हुआ था और जिसके कारण कुछ स्टोरेज वेरिएबल्स या अकाउंट बैलेंस में बदलाव आया था।

पहला एक स्टेट ट्रांज़िशन फ़ंक्शन $\phi$ है जो एक स्टेट (जैसे स्टोरेज वेरिएबल्स और अकाउंट बैलेंस), वातावरण (जैसे ब्लॉक टाइमस्टैम्प), और किसी लेनदेन के calldata को देखते हुए, एक नई स्टेट बनाता है:

यह फ़ंक्शन $\phi$ स्मार्ट कॉन्ट्रैक्ट के बाइटकोड का एक गणितीय प्रतिनिधित्व है। फिर, हमारे स्पेसिफिकेशन “सभी बैलेंस का योग कुल सप्लाई के बराबर होता है” को निम्नलिखित गणितीय सूत्र में संकलित (compile) किया जाएगा:

दूसरे शब्दों में, किसी भी स्टेट $i$ के लिए, प्रत्येक अकाउंट $a$ के लिए उस स्टेट में बैलेंस का योग $\left(\sum_a\texttt{state}_i\texttt{.balances}_a\right)$ उस स्टेट की total_supply के बराबर होता है।

अब मान लें कि हमें एक स्टेट ट्रांज़िशन फ़ंक्शन $\phi:\texttt{state}\rightarrow\texttt{state}'$ दिया गया है। हम यह जानना चाहते हैं कि यदि, उपरोक्त सूत्र का पालन करने वाले किसी भी $\texttt{state}$ को $\phi$ में प्लग किया जाता है, तो क्या परिणामी स्टेट $\texttt{state}'$ भी सूत्र का पालन करती है। (ध्यान दें कि हमारा स्पेसिफिकेशन $\phi$ से स्वतंत्र है)।

तब प्रूवर इंडक्शन (induction) द्वारा यह साबित करने का प्रयास करेगा (चिंता न करें यदि यह शब्द अपरिचित है — हम इसके बारे में बाद के अध्याय में बात करेंगे) कि यदि $\texttt{state}_i$ उपरोक्त स्पेसिफिकेशन का पालन करता है, तो बाद में आने वाली किसी भी स्टेट को भी इस स्पेसिफिकेशन का पालन करना चाहिए।

$\phi$ स्वयं स्मार्ट कॉन्ट्रैक्ट है, क्योंकि यह एक स्टेट, calldata, और एक वातावरण लेता है और एक नई स्टेट बनाता है। हमने ऊपर जो सूत्र लिखा है वह एक प्रॉपर्टी है जिसे हम यह सुनिश्चित करना चाहते हैं कि स्मार्ट कॉन्ट्रैक्ट में हो।

अतिरिक्त लाभ के रूप में, यदि कोई $\text{state}$ और $\texttt{calldata}$ है जो उल्लंघन का कारण बनता है, तो Certora Prover इसका एक उदाहरण प्रदान करेगा।

Certora Prover जैसे स्वचालित औपचारिक सत्यापन टूल का एक बड़ा लाभ यह है कि यह स्मार्ट कॉन्ट्रैक्ट के बाइटकोड को स्टेट वेरिएबल्स, calldata, और एनवायरनमेंट वेरिएबल्स के गणितीय फ़ंक्शन में अनुवादित करके हमारे लिए फ़ंक्शन $\phi$ का पता लगाता है। यह एक अत्यधिक जटिल प्रक्रिया है जिसके लिए पर्याप्त रिसर्च और डेवलपमेंट की आवश्यकता होती है, लेकिन शुक्र है कि हम इसे मुख्य रूप से एक ब्लैक बॉक्स के रूप में मान सकते हैं (कुछ महत्वपूर्ण अपवाद हैं जिन्हें हम बाद में एक्सप्लोर करेंगे)।

उदाहरण स्पेसिफिकेशन

हमारे उदाहरण “यदि कोई समय नहीं बीता है तो ऋणदाताओं को कोई ब्याज नहीं मिलना चाहिए” का उपयोग करके इसे गणितीय रूप से इस प्रकार व्यक्त किया जा सकता है:

इसका अर्थ यह है कि “यदि स्टेट्स $i$ और $j$ के ब्लॉक टाइमस्टैम्प समान हैं, तो interestEarned समान होना चाहिए।”

अगर गणित पढ़ने में थोड़ा अजीब लगे तो चिंता न करें। हम इसका अनुवाद इस प्रकार कर सकते हैं:

• $\forall_{i,j}$ का मतलब है “सभी $i$ और $j$ के लिए” या “$i$ और $j$ के किन्हीं दो मानों के लिए”
• $\texttt{state}_i\texttt{.timestamp}\texttt{ == } \texttt{state}_j\texttt{.timestamp}\rightarrow$ यदि उन दो स्टेट्स का टाइमस्टैम्प समान है
• $\texttt{state}_i\texttt{.interestEarned == }\texttt{state}_j\texttt{.interestEarned}$ तो interestEarned समान है

ध्यान दें कि $\rightarrow$ सामान्य प्रोग्रामिंग में “if then” की तरह व्यवहार करता है। Certora द्वारा उपयोग किया जाने वाला वास्तविक सिंटैक्स ऊपर दिए गए गणित की तुलना में Solidity जैसा अधिक दिखता है, लेकिन मूल अर्थ वही होगा।

औपचारिक सत्यापन (Formal Verification) बनाम फ़ज़िंग (Fuzzing)

औपचारिक सत्यापन और फ़ज़िंग एक ही उद्देश्य को पूरा करते हैं, लेकिन एक ही लक्ष्य को प्राप्त करने के लिए अलग-अलग रणनीतियों का उपयोग करते हैं। फ़ज़िंग इनवेरिएंट्स (invariants) के उल्लंघनों को खोजने का प्रयास करने के लिए लेनदेन के एक यादृच्छिक (random), लेकिन अक्सर निर्देशित, अनुक्रम का उपयोग करती है। वे ऐसा हजारों, संभवतः लाखों परीक्षण चलाकर करते हैं।

दूसरी ओर, औपचारिक सत्यापन गणितीय रूप से साबित करता है कि इनवेरिएंट्स लागू होते हैं।

इसके विपरीत, फ़ज़िंग बग्स की अनुपस्थिति को साबित नहीं कर सकती है। यह केवल यह दिखा सकती है कि जिन मामलों का इसने परीक्षण किया, उनमें बग अनुपस्थित था।

फ़ज़िंग हजारों या लाखों यादृच्छिक मामलों के लिए स्मार्ट कॉन्ट्रैक्ट का परीक्षण करती है। औपचारिक सत्यापन इनपुट्स और स्टोरेज वेरिएबल मानों के हर संभव संयोजन के लिए परीक्षण करता है।

औपचारिक सत्यापन की सीमाएँ

औपचारिक सत्यापन अनिवार्य रूप से स्वचालित रूप से गणितीय प्रमाण लिखना है — और यह काफी शक्तिशाली हो सकता है।

उदाहरण के लिए, कंप्यूटर ने निम्नलिखित को साबित किया है या साबित करने में महत्वपूर्ण भूमिका निभाई है (उदाहरण Computer Assisted Proofs पर विकिपीडिया लेख से लिए गए हैं):

• किसी भी 2D मानचित्र को चार रंगों में रंगा जा सकता है (four-colored)
• गेम Connect-4 में जो भी पहले चलता है वह हमेशा जीतता है, बशर्ते कि वे इष्टतम चाल (optimal move) चलें
• केप्लर कंजंक्चर (Kepler Conjecture) सत्य है — यदि गोले (spheres) को एक बॉक्स में रखा जाता है, तो पैक किए गए गोलों द्वारा लिए गए आयतन का बॉक्स के कुल आयतन पर उच्चतम घनत्व $\frac{\pi}{3\sqrt{2}}$ से अधिक नहीं हो सकता है।
• एक रूबिक्स क्यूब (Rubik’s Cube) को अधिकतम 20 चालों में हल किया जा सकता है

जैसा कि ऊपर देखा जा सकता है, कंप्यूटर-सहायता प्राप्त गणितीय प्रमाण बेहद शक्तिशाली हो सकते हैं, लेकिन वे उन पर फेंकी गई किसी भी समस्या को हल नहीं कर सकते हैं (यदि वे कर सकते हैं, तो गणित में कोई और अनसुलझी समस्या नहीं होगी)।

औपचारिक सत्यापन का उपयोग करने के लिए आपको बहुत अधिक गणित जानने की आवश्यकता नहीं है

भले ही आपने अपने जीवन में कभी कोई गणितीय प्रमाण नहीं लिखा हो, फिर भी आप Certora Prover का उपयोग कर सकते हैं। लगभग हर चीज डेवलपर से एब्सट्रैक्ट (abstracted) कर ली गई है, और डेवलपर्स Solidity के समान भाषा का उपयोग करके स्पेसिफिकेशन्स को परिभाषित कर सकते हैं।

हालाँकि, Prover क्या कर रहा है, इसके बारे में कुछ विचार होना अभी भी सहायक है। उदाहरण के लिए, कोई यह जाने बिना कि EVM कैसे काम करता है, स्मार्ट कॉन्ट्रैक्ट्स लिख और ऑडिट कर सकता है, लेकिन इससे अक्षम (inefficient) कोड बन सकता है। इसी तरह, पर्दे के पीछे क्या चल रहा है इसके कुछ विचार के बिना Certora Prover के लिए स्पेसिफिकेशन्स लिखने से ऐसे प्रमाण बन सकते हैं जिन्हें उत्पन्न होने में बहुत लंबा समय लगता है।

ठीक उसी तरह जैसे आप उच्च लागत के कारण किसी jpeg को EVM स्टोरेज वेरिएबल्स में स्टोर करने का प्रयास नहीं करेंगे, वैसे ही औपचारिक सत्यापन का उपयोग करते समय कुछ कमियां (pitfalls) हैं जिनसे आपको सचेत रूप से बचना चाहिए।

यहाँ औपचारिक सत्यापन की कुछ मूलभूत सीमाएँ दी गई हैं:

1. हॉल्टिंग प्रॉब्लम (The Halting Problem) — एक आर्बिट्रेरी प्रोग्राम दिए जाने पर, अनंत लूप्स का मज़बूती से पता लगाना गणितीय रूप से असंभव है।

यदि हम अनंत लूप्स का पता लगा सकते हैं, तो हम गणित में एक खुले प्रश्न, ट्विन प्राइम कंजंक्चर (twin prime conjecture) को आसानी से हल कर सकते हैं। ट्विन प्राइम के उदाहरण हैं (3,5), (11,13), (17,19) — इनमें दो का अंतर होता है।

खुला प्रश्न यह है कि क्या इन प्राइम्स की अनंत संख्या मौजूद है। यदि हम मज़बूती से अनंत लूप्स का पता लगा सकते हैं, तो हम एक ऐसा प्रोग्राम लिख सकते हैं जो सबसे बड़े संभव ट्विन प्राइम की खोज करता है और फिर रुक जाता है (halts)। यदि प्रोग्राम कभी नहीं रुकता है, तो हम जानते हैं कि ट्विन प्राइम्स की एक अनंत संख्या मौजूद है।

2. क्रिप्टोग्राफी (Cryptography) — एक 32-बाइट अनुक्रम दिए जाने पर जो कथित तौर पर किसी हैश का आउटपुट है, क्या उस हैश का प्री-इमेज (pre-image) मौजूद है? हैशेज़ के लिए प्री-इमेज खोजना बेहद कठिन (सभी व्यावहारिक उद्देश्यों के लिए, असंभव) है। कंप्यूटर-सहायता प्राप्त प्रमाण हमें उनकी कठोरता को तोड़ने नहीं देते हैं।

3. समीकरणों के बड़े गैर-रैखिक सिस्टम (Large non-linear systems of equations) — बहुत सारे वेरिएबल्स वाले समीकरणों के गैर-रैखिक (non-linear) सिस्टम को थोड़े समय में हल करना कठिन है। यहाँ, “रैखिक (linear)” का अर्थ है कि जिन वेरिएबल्स को हम हल कर रहे हैं उन्हें केवल कांस्टेंट्स से गुणा किया जाता है या अन्य अज्ञात वेरिएबल्स में जोड़ा जाता है।

यदि दो अज्ञात वेरिएबल्स को एक साथ गुणा किया जाता है, या उन्हें किसी घात तक बढ़ाया जाता है, तो हमारे पास समीकरणों का एक गैर-रैखिक सिस्टम होता है। यदि किसी औपचारिक सत्यापन टूल को अप्रत्यक्ष रूप से समीकरणों के एक गैर-रैखिक सिस्टम को हल करना होता है, तो वह टूल समाधान खोजने में अत्यधिक समय बिता सकता है।

यह ट्यूटोरियल सीरीज़ कैसे संरचित (structured) है

यह ट्यूटोरियल सीरीज़ निम्न पर केंद्रित है:

1. Certora Prover के लिए स्पेसिफिकेशन्स कैसे लिखें, उसका सिंटैक्स
2. आपके स्वयं के उपयोग के लिए पैटर्न-मैच करने हेतु पर्याप्त उदाहरण
3. स्पेसिफिकेशन में बग्स से कैसे बचें
4. वास्तविक DeFi प्रोटोकॉल्स का औपचारिक रूप से सत्यापन कैसे करें

श्रृंखला का प्रत्येक भाग पिछले अध्यायों की अवधारणाओं पर आधारित है। इस कारण से, हम पाठकों को सलाह देते हैं कि वे इधर-उधर कूदने के बजाय क्रम में श्रृंखला का पालन करें।

यह लेख Certora Prover का उपयोग करके औपचारिक सत्यापन पर एक श्रृंखला का हिस्सा है।