स्मार्ट अनुबंधों का औपचारिक सत्यापन

स्मार्ट अनुबंध विकेंद्रीकृत, विश्वासहीन और मजबूत एप्लिकेशन बनाना संभव बना रहे हैं जो नए उपयोग-मामले पेश करते हैं और उपयोगकर्ताओं के लिए मूल्य अनलॉक करते हैं। क्योंकि स्मार्ट अनुबंध बड़ी मात्रा में मूल्य को संभालते हैं, इसलिए डेवलपर्स के लिए सुरक्षा एक महत्वपूर्ण विचार है।

औपचारिक सत्यापन स्मार्ट अनुबंध सुरक्षा में सुधार के लिए अनुशंसित तकनीकों में से एक है। औपचारिक सत्यापन, जो प्रोग्राम को निर्दिष्ट करने, डिज़ाइन करने और सत्यापित करने के लिए औपचारिक विधियों (opens in a new tab) का उपयोग करता है, का उपयोग वर्षों से महत्वपूर्ण हार्डवेयर और सॉफ़्टवेयर सिस्टम की शुद्धता सुनिश्चित करने के लिए किया जाता रहा है।

जब स्मार्ट अनुबंधों में लागू किया जाता है, तो औपचारिक सत्यापन यह साबित कर सकता है कि अनुबंध का व्यावसायिक तर्क एक पूर्वनिर्धारित विनिर्देश को पूरा करता है। अनुबंध कोड की शुद्धता का आकलन करने के अन्य तरीकों, जैसे कि परीक्षण की तुलना में, औपचारिक सत्यापन मजबूत गारंटी देता है कि एक स्मार्ट अनुबंध कार्यात्मक रूप से सही है।

औपचारिक सत्यापन क्या है?

औपचारिक सत्यापन एक औपचारिक विनिर्देश के संबंध में किसी सिस्टम की शुद्धता का मूल्यांकन करने की प्रक्रिया को संदर्भित करता है। सरल शब्दों में, औपचारिक सत्यापन हमें यह जांचने की अनुमति देता है कि क्या किसी सिस्टम का व्यवहार कुछ आवश्यकताओं को पूरा करता है (यानी, यह वही करता है जो हम चाहते हैं)।

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

औपचारिक मॉडल क्या है?

कंप्यूटर विज्ञान में, एक औपचारिक मॉडल (opens in a new tab) एक कम्प्यूटेशनल प्रक्रिया का गणितीय विवरण है। प्रोग्रामों को गणितीय कार्यों (समीकरणों) में अमूर्त किया जाता है, जिसमें मॉडल यह वर्णन करता है कि इनपुट दिए जाने पर कार्यों के आउटपुट की गणना कैसे की जाती है।

औपचारिक मॉडल अमूर्तता का एक स्तर प्रदान करते हैं जिस पर किसी प्रोग्राम के व्यवहार के विश्लेषण का मूल्यांकन किया जा सकता है। औपचारिक मॉडलों का अस्तित्व एक औपचारिक विनिर्देश के निर्माण की अनुमति देता है, जो विचाराधीन मॉडल के वांछित गुणों का वर्णन करता है।

औपचारिक सत्यापन के लिए स्मार्ट अनुबंधों की मॉडलिंग के लिए विभिन्न तकनीकों का उपयोग किया जाता है। उदाहरण के लिए, कुछ मॉडलों का उपयोग स्मार्ट अनुबंध के उच्च-स्तरीय व्यवहार के बारे में तर्क करने के लिए किया जाता है। ये मॉडलिंग तकनीकें स्मार्ट अनुबंधों पर एक ब्लैक-बॉक्स दृष्टिकोण लागू करती हैं, उन्हें ऐसे सिस्टम के रूप में देखती हैं जो इनपुट स्वीकार करते हैं और उन इनपुट के आधार पर गणना निष्पादित करते हैं।

उच्च-स्तरीय मॉडल स्मार्ट अनुबंधों और बाहरी एजेंटों, जैसे बाह्य रूप से स्वामित्व वाले खातों (EOAs), अनुबंध खातों और ब्लॉकचेन वातावरण के बीच संबंधों पर ध्यान केंद्रित करते हैं। ऐसे मॉडल उन गुणों को परिभाषित करने के लिए उपयोगी होते हैं जो निर्दिष्ट करते हैं कि कुछ उपयोगकर्ता इंटरैक्शन के जवाब में अनुबंध को कैसा व्यवहार करना चाहिए।

इसके विपरीत, अन्य औपचारिक मॉडल स्मार्ट अनुबंध के निम्न-स्तरीय व्यवहार पर ध्यान केंद्रित करते हैं। जबकि उच्च-स्तरीय मॉडल अनुबंध की कार्यक्षमता के बारे में तर्क करने में मदद कर सकते हैं, वे कार्यान्वयन की आंतरिक कार्यप्रणाली के बारे में विवरण प्राप्त करने में विफल हो सकते हैं। निम्न-स्तरीय मॉडल प्रोग्राम विश्लेषण के लिए एक व्हाइट-बॉक्स दृष्टिकोण लागू करते हैं और अनुबंध के निष्पादन के लिए प्रासंगिक गुणों के बारे में तर्क करने के लिए स्मार्ट अनुबंध अनुप्रयोगों के निम्न-स्तरीय प्रतिनिधित्व, जैसे प्रोग्राम ट्रेस और नियंत्रण प्रवाह ग्राफ़ (opens in a new tab) पर भरोसा करते हैं।

निम्न-स्तरीय मॉडल को आदर्श माना जाता है क्योंकि वे इथेरियम के निष्पादन वातावरण (यानी, EVM) में एक स्मार्ट अनुबंध के वास्तविक निष्पादन का प्रतिनिधित्व करते हैं। निम्न-स्तरीय मॉडलिंग तकनीकें विशेष रूप से स्मार्ट अनुबंधों में महत्वपूर्ण सुरक्षा गुणों को स्थापित करने और संभावित कमजोरियों का पता लगाने में उपयोगी होती हैं।

औपचारिक विनिर्देश क्या है?

एक विनिर्देश केवल एक तकनीकी आवश्यकता है जिसे किसी विशेष सिस्टम को पूरा करना चाहिए। प्रोग्रामिंग में, विनिर्देश किसी प्रोग्राम के निष्पादन के बारे में सामान्य विचारों का प्रतिनिधित्व करते हैं (यानी, प्रोग्राम को क्या करना चाहिए)।

स्मार्ट अनुबंधों के संदर्भ में, औपचारिक विनिर्देश गुणों को संदर्भित करते हैं—उन आवश्यकताओं का औपचारिक विवरण जिन्हें एक अनुबंध को पूरा करना चाहिए। ऐसे गुणों को "इनवेरिएंट्स" के रूप में वर्णित किया जाता है और ये अनुबंध के निष्पादन के बारे में तार्किक दावों का प्रतिनिधित्व करते हैं जो बिना किसी अपवाद के हर संभव परिस्थिति में सत्य रहने चाहिए।

इस प्रकार, हम एक औपचारिक विनिर्देश को एक औपचारिक भाषा में लिखे गए कथनों के संग्रह के रूप में सोच सकते हैं जो एक स्मार्ट अनुबंध के इच्छित निष्पादन का वर्णन करते हैं। विनिर्देश एक अनुबंध के गुणों को कवर करते हैं और परिभाषित करते हैं कि अनुबंध को विभिन्न परिस्थितियों में कैसा व्यवहार करना चाहिए। औपचारिक सत्यापन का उद्देश्य यह निर्धारित करना है कि क्या एक स्मार्ट अनुबंध में ये गुण (इनवेरिएंट्स) हैं और निष्पादन के दौरान इन गुणों का उल्लंघन नहीं किया जाता है।

स्मार्ट अनुबंधों के सुरक्षित कार्यान्वयन को विकसित करने में औपचारिक विनिर्देश महत्वपूर्ण हैं। जो अनुबंध इनवेरिएंट्स को लागू करने में विफल रहते हैं या निष्पादन के दौरान उनके गुणों का उल्लंघन होता है, वे उन कमजोरियों के प्रति संवेदनशील होते हैं जो कार्यक्षमता को नुकसान पहुंचा सकते हैं या दुर्भावनापूर्ण कारनामों का कारण बन सकते हैं।

स्मार्ट अनुबंधों के लिए औपचारिक विनिर्देशों के प्रकार

औपचारिक विनिर्देश प्रोग्राम निष्पादन की शुद्धता के बारे में गणितीय तर्क को सक्षम करते हैं। औपचारिक मॉडलों की तरह, औपचारिक विनिर्देश या तो उच्च-स्तरीय गुणों या अनुबंध कार्यान्वयन के निम्न-स्तरीय व्यवहार को कैप्चर कर सकते हैं।

औपचारिक विनिर्देश प्रोग्राम लॉजिक (opens in a new tab) के तत्वों का उपयोग करके प्राप्त किए जाते हैं, जो किसी प्रोग्राम के गुणों के बारे में औपचारिक तर्क की अनुमति देते हैं। एक प्रोग्राम लॉजिक में औपचारिक नियम होते हैं जो (गणितीय भाषा में) किसी प्रोग्राम के अपेक्षित व्यवहार को व्यक्त करते हैं। औपचारिक विनिर्देश बनाने में विभिन्न प्रोग्राम लॉजिक्स का उपयोग किया जाता है, जिनमें रीचेबिलिटी लॉजिक (opens in a new tab), टेम्पोरल लॉजिक (opens in a new tab), और Hoare लॉजिक (opens in a new tab) शामिल हैं।

स्मार्ट अनुबंधों के लिए औपचारिक विनिर्देशों को मोटे तौर पर उच्च-स्तरीय या निम्न-स्तरीय विनिर्देशों के रूप में वर्गीकृत किया जा सकता है। भले ही कोई विनिर्देश किस श्रेणी का हो, उसे विश्लेषण के तहत सिस्टम की संपत्ति का पर्याप्त और स्पष्ट रूप से वर्णन करना चाहिए।

उच्च-स्तरीय विनिर्देश

जैसा कि नाम से पता चलता है, एक उच्च-स्तरीय विनिर्देश (जिसे "मॉडल-उन्मुख विनिर्देश" भी कहा जाता है) किसी प्रोग्राम के उच्च-स्तरीय व्यवहार का वर्णन करता है। उच्च-स्तरीय विनिर्देश एक स्मार्ट अनुबंध को परिमित स्थिति मशीन (opens in a new tab) (FSM) के रूप में मॉडल करते हैं, जो संचालन करके स्थितियों के बीच संक्रमण कर सकता है, जिसमें FSM मॉडल के लिए औपचारिक गुणों को परिभाषित करने के लिए टेम्पोरल लॉजिक का उपयोग किया जाता है।

टेम्पोरल लॉजिक्स (opens in a new tab) "समय के संदर्भ में योग्य प्रस्तावों के बारे में तर्क करने के नियम हैं (उदा., "मैं हमेशा भूखा रहता हूँ" या "मैं अंततः भूखा रहूँगा")।" जब औपचारिक सत्यापन पर लागू किया जाता है, तो टेम्पोरल लॉजिक्स का उपयोग स्थिति-मशीनों के रूप में मॉडल किए गए सिस्टम के सही व्यवहार के बारे में दावों को बताने के लिए किया जाता है। विशेष रूप से, एक टेम्पोरल लॉजिक भविष्य की स्थितियों का वर्णन करता है जिसमें एक स्मार्ट अनुबंध हो सकता है और यह स्थितियों के बीच कैसे संक्रमण करता है।

उच्च-स्तरीय विनिर्देश आम तौर पर स्मार्ट अनुबंधों के लिए दो महत्वपूर्ण टेम्पोरल गुणों को कैप्चर करते हैं: सुरक्षा और जीवंतता। सुरक्षा गुण इस विचार का प्रतिनिधित्व करते हैं कि "कभी कुछ बुरा नहीं होता" और आमतौर पर इनवेरिएंस व्यक्त करते हैं। एक सुरक्षा गुण सामान्य सॉफ़्टवेयर आवश्यकताओं को परिभाषित कर सकता है, जैसे डेडॉक (opens in a new tab) से स्वतंत्रता, या अनुबंधों के लिए डोमेन-विशिष्ट गुणों को व्यक्त कर सकता है (उदा., कार्यों के लिए एक्सेस कंट्रोल पर इनवेरिएंट्स, स्थिति चर के स्वीकार्य मान, या टोकन ट्रांसफर के लिए शर्तें)।

उदाहरण के लिए इस सुरक्षा आवश्यकता को लें जो ERC-20 टोकन अनुबंधों में transfer() या transferFrom() का उपयोग करने की शर्तों को कवर करती है: "प्रेषक का बैलेंस कभी भी भेजे जाने वाले टोकन की अनुरोधित राशि से कम नहीं होता है।"। अनुबंध इनवेरिएंट के इस प्राकृतिक-भाषा विवरण को एक औपचारिक (गणितीय) विनिर्देश में अनुवादित किया जा सकता है, जिसे बाद में वैधता के लिए कड़ाई से जांचा जा सकता है।

जीवंतता गुण यह दावा करते हैं कि "अंततः कुछ अच्छा होता है" और विभिन्न स्थितियों के माध्यम से प्रगति करने की अनुबंध की क्षमता से संबंधित हैं। जीवंतता गुण का एक उदाहरण "तरलता" है, जो अनुरोध पर उपयोगकर्ताओं को अपने बैलेंस ट्रांसफर करने की अनुबंध की क्षमता को संदर्भित करता है। यदि इस गुण का उल्लंघन किया जाता है, तो उपयोगकर्ता अनुबंध में संग्रहीत संपत्तियों को वापस लेने में असमर्थ होंगे, जैसा कि Parity वॉलेट घटना (opens in a new tab) के साथ हुआ था।

निम्न-स्तरीय विनिर्देश

उच्च-स्तरीय विनिर्देश एक अनुबंध के परिमित-स्थिति मॉडल को प्रारंभिक बिंदु के रूप में लेते हैं और इस मॉडल के वांछित गुणों को परिभाषित करते हैं। इसके विपरीत, निम्न-स्तरीय विनिर्देश (जिन्हें "संपत्ति-उन्मुख विनिर्देश" भी कहा जाता है) अक्सर प्रोग्रामों (स्मार्ट अनुबंधों) को गणितीय कार्यों के संग्रह वाले सिस्टम के रूप में मॉडल करते हैं और ऐसे सिस्टम के सही व्यवहार का वर्णन करते हैं।

सरल शब्दों में, निम्न-स्तरीय विनिर्देश प्रोग्राम ट्रेस का विश्लेषण करते हैं और इन ट्रेस पर एक स्मार्ट अनुबंध के गुणों को परिभाषित करने का प्रयास करते हैं। ट्रेस फ़ंक्शन निष्पादन के अनुक्रमों को संदर्भित करते हैं जो एक स्मार्ट अनुबंध की स्थिति को बदलते हैं; इसलिए, निम्न-स्तरीय विनिर्देश अनुबंध के आंतरिक निष्पादन के लिए आवश्यकताओं को निर्दिष्ट करने में मदद करते हैं।

निम्न-स्तरीय औपचारिक विनिर्देशों को या तो Hoare-शैली के गुणों या निष्पादन पथों पर इनवेरिएंट्स के रूप में दिया जा सकता है।

Hoare-शैली के गुण

Hoare लॉजिक (opens in a new tab) स्मार्ट अनुबंधों सहित प्रोग्रामों की शुद्धता के बारे में तर्क करने के लिए औपचारिक नियमों का एक सेट प्रदान करता है। एक Hoare-शैली की संपत्ति को Hoare ट्रिपल {P}c{Q} द्वारा दर्शाया जाता है, जहां c एक प्रोग्राम है और P और Q c (यानी, प्रोग्राम) की स्थिति पर प्रेडिकेट्स हैं, जिन्हें औपचारिक रूप से क्रमशः पूर्व-शर्तों और पश्च-शर्तों के रूप में वर्णित किया गया है।

एक पूर्व-शर्त एक प्रेडिकेट है जो किसी फ़ंक्शन के सही निष्पादन के लिए आवश्यक शर्तों का वर्णन करता है; अनुबंध में कॉल करने वाले उपयोगकर्ताओं को इस आवश्यकता को पूरा करना चाहिए। एक पश्च-शर्त एक प्रेडिकेट है जो उस स्थिति का वर्णन करता है जिसे एक फ़ंक्शन स्थापित करता है यदि सही ढंग से निष्पादित किया जाता है; उपयोगकर्ता फ़ंक्शन में कॉल करने के बाद इस स्थिति के सत्य होने की उम्मीद कर सकते हैं। Hoare लॉजिक में एक इनवेरिएंट एक प्रेडिकेट है जो किसी फ़ंक्शन के निष्पादन द्वारा संरक्षित होता है (यानी, यह नहीं बदलता है)।

Hoare-शैली के विनिर्देश या तो आंशिक शुद्धता या पूर्ण शुद्धता की गारंटी दे सकते हैं। एक अनुबंध फ़ंक्शन का कार्यान्वयन "आंशिक रूप से सही" है यदि फ़ंक्शन निष्पादित होने से पहले पूर्व-शर्त सत्य है, और यदि निष्पादन समाप्त हो जाता है, तो पश्च-शर्त भी सत्य है। पूर्ण शुद्धता का प्रमाण तब प्राप्त होता है जब फ़ंक्शन निष्पादित होने से पहले एक पूर्व-शर्त सत्य होती है, निष्पादन समाप्त होने की गारंटी होती है और जब ऐसा होता है, तो पश्च-शर्त सत्य होती है।

पूर्ण शुद्धता का प्रमाण प्राप्त करना मुश्किल है क्योंकि कुछ निष्पादन समाप्त होने से पहले देरी कर सकते हैं, या कभी समाप्त नहीं हो सकते हैं। इसके बावजूद, यह सवाल कि क्या निष्पादन समाप्त होता है, यकीनन एक विवादास्पद बिंदु है क्योंकि इथेरियम का गैस तंत्र अनंत प्रोग्राम लूप को रोकता है (निष्पादन या तो सफलतापूर्वक समाप्त होता है या 'आउट-ऑफ़-गैस' त्रुटि के कारण समाप्त होता है)।

Hoare लॉजिक का उपयोग करके बनाए गए स्मार्ट अनुबंध विनिर्देशों में अनुबंध में कार्यों और लूप के निष्पादन के लिए पूर्व-शर्तें, पश्च-शर्तें और इनवेरिएंट्स परिभाषित होंगे। पूर्व-शर्तों में अक्सर किसी फ़ंक्शन में गलत इनपुट की संभावना शामिल होती है, जिसमें पश्च-शर्तें ऐसे इनपुट के अपेक्षित प्रतिक्रिया का वर्णन करती हैं (उदा., एक विशिष्ट अपवाद फेंकना)। इस तरह Hoare-शैली के गुण अनुबंध कार्यान्वयन की शुद्धता सुनिश्चित करने के लिए प्रभावी हैं।

कई औपचारिक सत्यापन फ्रेमवर्क कार्यों की अर्थपूर्ण शुद्धता साबित करने के लिए Hoare-शैली के विनिर्देशों का उपयोग करते हैं। Solidity में require और assert कथनों का उपयोग करके सीधे अनुबंध कोड में Hoare-शैली के गुणों (दावों के रूप में) को जोड़ना भी संभव है।

require कथन एक पूर्व-शर्त या इनवेरिएंट व्यक्त करते हैं और अक्सर उपयोगकर्ता इनपुट को मान्य करने के लिए उपयोग किए जाते हैं, जबकि assert सुरक्षा के लिए आवश्यक पश्च-शर्त को कैप्चर करता है। उदाहरण के लिए, कार्यों के लिए उचित एक्सेस कंट्रोल (सुरक्षा संपत्ति का एक उदाहरण) कॉलिंग खाते की पहचान पर पूर्व-शर्त जांच के रूप में require का उपयोग करके प्राप्त किया जा सकता है। इसी तरह, एक अनुबंध में स्थिति चर के स्वीकार्य मानों पर एक इनवेरिएंट (उदा., संचलन में टोकन की कुल संख्या) को फ़ंक्शन निष्पादन के बाद अनुबंध की स्थिति की पुष्टि करने के लिए assert का उपयोग करके उल्लंघन से बचाया जा सकता है।

ट्रेस-स्तरीय गुण

ट्रेस-आधारित विनिर्देश उन ऑपरेशनों का वर्णन करते हैं जो एक अनुबंध को विभिन्न स्थितियों के बीच संक्रमण करते हैं और इन ऑपरेशनों के बीच संबंधों का वर्णन करते हैं। जैसा कि पहले बताया गया है, ट्रेस ऑपरेशनों के अनुक्रम हैं जो किसी विशेष तरीके से अनुबंध की स्थिति को बदलते हैं।

यह दृष्टिकोण स्मार्ट अनुबंधों के मॉडल पर स्थिति-संक्रमण सिस्टम के रूप में निर्भर करता है जिसमें कुछ पूर्वनिर्धारित स्थितियां (स्थिति चर द्वारा वर्णित) और पूर्वनिर्धारित संक्रमणों का एक सेट (अनुबंध कार्यों द्वारा वर्णित) होता है। इसके अलावा, एक नियंत्रण प्रवाह ग्राफ़ (opens in a new tab) (CFG), जो किसी प्रोग्राम के निष्पादन प्रवाह का एक चित्रमय प्रतिनिधित्व है, अक्सर अनुबंध के परिचालन शब्दार्थ का वर्णन करने के लिए उपयोग किया जाता है। यहां, प्रत्येक ट्रेस को नियंत्रण प्रवाह ग्राफ़ पर एक पथ के रूप में दर्शाया गया है।

मुख्य रूप से, ट्रेस-स्तरीय विनिर्देशों का उपयोग स्मार्ट अनुबंधों में आंतरिक निष्पादन के पैटर्न के बारे में तर्क करने के लिए किया जाता है। ट्रेस-स्तरीय विनिर्देश बनाकर, हम एक स्मार्ट अनुबंध के लिए स्वीकार्य निष्पादन पथ (यानी, स्थिति संक्रमण) का दावा करते हैं। प्रतीकात्मक निष्पादन जैसी तकनीकों का उपयोग करके, हम औपचारिक रूप से सत्यापित कर सकते हैं कि निष्पादन कभी भी ऐसे पथ का अनुसरण नहीं करता है जो औपचारिक मॉडल में परिभाषित नहीं है।

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

फंड जमा करना
फंड जमा करने के बाद किसी प्रस्ताव पर वोट करना
यदि वे किसी प्रस्ताव पर वोट नहीं करते हैं तो रिफंड का दावा करना

उदाहरण ट्रेस-स्तरीय गुण हो सकते हैं "जो उपयोगकर्ता फंड जमा नहीं करते हैं वे किसी प्रस्ताव पर वोट नहीं कर सकते" या "जो उपयोगकर्ता किसी प्रस्ताव पर वोट नहीं करते हैं उन्हें हमेशा रिफंड का दावा करने में सक्षम होना चाहिए"। दोनों गुण निष्पादन के पसंदीदा अनुक्रमों का दावा करते हैं (फंड जमा करने से पहले वोटिंग नहीं हो सकती है और किसी प्रस्ताव पर वोट करने के बाद रिफंड का दावा नहीं किया जा सकता है)।

स्मार्ट अनुबंधों के औपचारिक सत्यापन के लिए तकनीकें

मॉडल चेकिंग

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

मॉडल चेकिंग के लिए एक सिस्टम (यानी, एक अनुबंध) का एक अमूर्त गणितीय प्रतिनिधित्व बनाने और प्रोपोज़िशनल लॉजिक (opens in a new tab) में निहित सूत्रों का उपयोग करके इस सिस्टम के गुणों को व्यक्त करने की आवश्यकता होती है। यह मॉडल-चेकिंग एल्गोरिदम के कार्य को सरल बनाता है, अर्थात् यह साबित करने के लिए कि एक गणितीय मॉडल दिए गए तार्किक सूत्र को संतुष्ट करता है।

औपचारिक सत्यापन में मॉडल चेकिंग का उपयोग मुख्य रूप से टेम्पोरल गुणों का मूल्यांकन करने के लिए किया जाता है जो समय के साथ अनुबंध के व्यवहार का वर्णन करते हैं। स्मार्ट अनुबंधों के लिए टेम्पोरल गुणों में सुरक्षा और जीवंतता शामिल हैं, जिन्हें हमने पहले समझाया था।

उदाहरण के लिए, एक्सेस कंट्रोल से संबंधित एक सुरक्षा संपत्ति (उदा., केवल अनुबंध का मालिक selfdestruct को कॉल कर सकता है) को औपचारिक लॉजिक में लिखा जा सकता है। उसके बाद, मॉडल-चेकिंग एल्गोरिदम यह सत्यापित कर सकता है कि क्या अनुबंध इस औपचारिक विनिर्देश को पूरा करता है।

मॉडल चेकिंग स्थिति स्थान अन्वेषण का उपयोग करता है, जिसमें एक स्मार्ट अनुबंध की सभी संभावित स्थितियों का निर्माण करना और उन पहुंच योग्य स्थितियों को खोजने का प्रयास करना शामिल है जो संपत्ति के उल्लंघन का परिणाम हैं। हालांकि, इससे अनंत संख्या में स्थितियां हो सकती हैं (जिसे "स्थिति विस्फोट समस्या" के रूप में जाना जाता है), इसलिए मॉडल चेकर्स स्मार्ट अनुबंधों के कुशल विश्लेषण को संभव बनाने के लिए अमूर्त तकनीकों पर भरोसा करते हैं।

प्रमेय सिद्ध करना

प्रमेय सिद्ध करना स्मार्ट अनुबंधों सहित प्रोग्रामों की शुद्धता के बारे में गणितीय रूप से तर्क करने की एक विधि है। इसमें अनुबंध के सिस्टम के मॉडल और उसके विनिर्देशों को गणितीय सूत्रों (तार्किक कथनों) में बदलना शामिल है।

प्रमेय सिद्ध करने का उद्देश्य इन कथनों के बीच तार्किक तुल्यता को सत्यापित करना है। "तार्किक तुल्यता" (जिसे "तार्किक द्वि-निहितार्थ" भी कहा जाता है) दो कथनों के बीच एक प्रकार का संबंध है जैसे कि पहला कथन सत्य है यदि और केवल यदि दूसरा कथन सत्य है।

अनुबंध के मॉडल और उसकी संपत्ति के बारे में कथनों के बीच आवश्यक संबंध (तार्किक तुल्यता) को एक सिद्ध करने योग्य कथन (जिसे प्रमेय कहा जाता है) के रूप में तैयार किया जाता है। अनुमान की एक औपचारिक प्रणाली का उपयोग करके, स्वचालित प्रमेय प्रमाणक प्रमेय की वैधता को सत्यापित कर सकता है। दूसरे शब्दों में, एक प्रमेय प्रमाणक निर्णायक रूप से साबित कर सकता है कि एक स्मार्ट अनुबंध का मॉडल उसके विनिर्देशों से बिल्कुल मेल खाता है।

जबकि मॉडल चेकिंग अनुबंधों को परिमित स्थितियों के साथ संक्रमण सिस्टम के रूप में मॉडल करता है, प्रमेय सिद्ध करना अनंत-स्थिति सिस्टम के विश्लेषण को संभाल सकता है। हालांकि, इसका मतलब है कि एक स्वचालित प्रमेय प्रमाणक हमेशा यह नहीं जान सकता कि कोई तार्किक समस्या "निर्णय योग्य" है या नहीं।

नतीजतन, शुद्धता प्रमाण प्राप्त करने में प्रमेय प्रमाणक का मार्गदर्शन करने के लिए अक्सर मानवीय सहायता की आवश्यकता होती है। प्रमेय सिद्ध करने में मानवीय प्रयास का उपयोग इसे मॉडल चेकिंग की तुलना में उपयोग करने के लिए अधिक महंगा बनाता है, जो पूरी तरह से स्वचालित है।

प्रतीकात्मक निष्पादन

प्रतीकात्मक निष्पादन ठोस मानों (उदा., x == 5) के बजाय प्रतीकात्मक मानों (उदा., x > 5) का उपयोग करके कार्यों को निष्पादित करके एक स्मार्ट अनुबंध का विश्लेषण करने की एक विधि है। एक औपचारिक सत्यापन तकनीक के रूप में, प्रतीकात्मक निष्पादन का उपयोग अनुबंध के कोड में ट्रेस-स्तरीय गुणों के बारे में औपचारिक रूप से तर्क करने के लिए किया जाता है।

प्रतीकात्मक निष्पादन प्रतीकात्मक इनपुट मानों पर एक गणितीय सूत्र के रूप में एक निष्पादन ट्रेस का प्रतिनिधित्व करता है, जिसे अन्यथा पथ प्रेडिकेट कहा जाता है। एक SMT समाधानकर्ता (opens in a new tab) का उपयोग यह जांचने के लिए किया जाता है कि क्या कोई पथ प्रेडिकेट "संतुष्ट करने योग्य" है (यानी, ऐसा कोई मान मौजूद है जो सूत्र को संतुष्ट कर सकता है)। यदि एक कमजोर पथ संतुष्ट करने योग्य है, तो SMT समाधानकर्ता एक ठोस मान उत्पन्न करेगा जो निष्पादन को उस पथ की ओर ले जाता है।

मान लीजिए कि एक स्मार्ट अनुबंध का फ़ंक्शन इनपुट के रूप में एक uint मान (x) लेता है और जब x 5 से अधिक और 10 से कम होता है तो वापस हो जाता है। एक सामान्य परीक्षण प्रक्रिया का उपयोग करके त्रुटि को ट्रिगर करने वाले x के लिए एक मान खोजने के लिए वास्तव में त्रुटि-ट्रिगरिंग इनपुट खोजने के आश्वासन के बिना दर्जनों परीक्षण मामलों (या अधिक) के माध्यम से चलने की आवश्यकता होगी।

इसके विपरीत, एक प्रतीकात्मक निष्पादन उपकरण प्रतीकात्मक मान के साथ फ़ंक्शन को निष्पादित करेगा: X > 5 ∧ X < 10 (यानी, x 5 से अधिक है और x 10 से कम है)। संबंधित पथ प्रेडिकेट x = X > 5 ∧ X < 10 को तब हल करने के लिए एक SMT समाधानकर्ता को दिया जाएगा। यदि कोई विशेष मान सूत्र x = X > 5 ∧ X < 10 को संतुष्ट करता है, तो SMT समाधानकर्ता इसकी गणना करेगा—उदाहरण के लिए, समाधानकर्ता x के मान के रूप में 7 उत्पन्न कर सकता है।

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

इसके अलावा, प्रतीकात्मक निष्पादन अन्य संपत्ति-आधारित तकनीकों (उदा., फ़ज़िंग) की तुलना में कम गलत सकारात्मक उत्पन्न करता है जो यादृच्छिक रूप से किसी फ़ंक्शन के लिए इनपुट उत्पन्न करते हैं। यदि प्रतीकात्मक निष्पादन के दौरान कोई त्रुटि स्थिति ट्रिगर होती है, तो एक ठोस मान उत्पन्न करना संभव है जो त्रुटि को ट्रिगर करता है और समस्या को पुन: उत्पन्न करता है।

प्रतीकात्मक निष्पादन शुद्धता का कुछ हद तक गणितीय प्रमाण भी प्रदान कर सकता है। ओवरफ़्लो सुरक्षा के साथ अनुबंध फ़ंक्शन के निम्नलिखित उदाहरण पर विचार करें:

function safe_add(uint x, uint y) returns(uint z){

  z = x + y;
  require(z>=x);
  require(z>=y);

  return z;
}

एक निष्पादन ट्रेस जिसके परिणामस्वरूप एक पूर्णांक ओवरफ़्लो होता है, उसे सूत्र को संतुष्ट करने की आवश्यकता होगी: z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y) ऐसे सूत्र के हल होने की संभावना नहीं है, इसलिए यह एक गणितीय प्रमाण के रूप में कार्य करता है कि फ़ंक्शन safe_add कभी ओवरफ़्लो नहीं होता है।

स्मार्ट अनुबंधों के लिए औपचारिक सत्यापन का उपयोग क्यों करें?

विश्वसनीयता की आवश्यकता

औपचारिक सत्यापन का उपयोग सुरक्षा-महत्वपूर्ण सिस्टम की शुद्धता का आकलन करने के लिए किया जाता है जिनकी विफलता के विनाशकारी परिणाम हो सकते हैं, जैसे मृत्यु, चोट, या वित्तीय बर्बादी। स्मार्ट अनुबंध उच्च-मूल्य वाले एप्लिकेशन हैं जो भारी मात्रा में मूल्य को नियंत्रित करते हैं, और डिज़ाइन में सरल त्रुटियां उपयोगकर्ताओं के लिए अपूरणीय नुकसान (opens in a new tab) का कारण बन सकती हैं। हालांकि, तैनाती से पहले एक अनुबंध को औपचारिक रूप से सत्यापित करने से यह गारंटी बढ़ सकती है कि यह ब्लॉकचेन पर चलने के बाद उम्मीद के मुताबिक प्रदर्शन करेगा।

किसी भी स्मार्ट अनुबंध में विश्वसनीयता एक अत्यधिक वांछित गुण है, खासकर क्योंकि इथेरियम वर्चुअल मशीन (EVM) में तैनात कोड आमतौर पर अपरिवर्तनीय होता है। लॉन्च के बाद के अपग्रेड आसानी से सुलभ नहीं होने के कारण, अनुबंधों की विश्वसनीयता की गारंटी देने की आवश्यकता औपचारिक सत्यापन को आवश्यक बनाती है। औपचारिक सत्यापन मुश्किल मुद्दों का पता लगाने में सक्षम है, जैसे कि पूर्णांक अंडरफ़्लो और ओवरफ़्लो, री-एंट्रेंसी, और खराब गैस अनुकूलन, जो ऑडिटर्स और परीक्षकों से बच सकते हैं।

कार्यात्मक शुद्धता साबित करें

प्रोग्राम परीक्षण यह साबित करने का सबसे आम तरीका है कि एक स्मार्ट अनुबंध कुछ आवश्यकताओं को पूरा करता है। इसमें उस डेटा के नमूने के साथ एक अनुबंध को निष्पादित करना शामिल है जिसे संभालने की उम्मीद है और इसके व्यवहार का विश्लेषण करना है। यदि अनुबंध नमूना डेटा के लिए अपेक्षित परिणाम देता है, तो डेवलपर्स के पास इसकी शुद्धता का वस्तुनिष्ठ प्रमाण होता है।

हालांकि, यह दृष्टिकोण उन इनपुट मानों के लिए सही निष्पादन साबित नहीं कर सकता है जो नमूने का हिस्सा नहीं हैं। इसलिए, एक अनुबंध का परीक्षण बग का पता लगाने में मदद कर सकता है (यानी, यदि कुछ कोड पथ निष्पादन के दौरान वांछित परिणाम देने में विफल रहते हैं), लेकिन यह निर्णायक रूप से बग की अनुपस्थिति को साबित नहीं कर सकता है।

इसके विपरीत, औपचारिक सत्यापन औपचारिक रूप से यह साबित कर सकता है कि एक स्मार्ट अनुबंध अनुबंध को बिल्कुल भी चलाए बिना निष्पादन की एक अनंत सीमा के लिए आवश्यकताओं को पूरा करता है। इसके लिए एक औपचारिक विनिर्देश बनाने की आवश्यकता होती है जो सही अनुबंध व्यवहारों का सटीक वर्णन करता है और अनुबंध के सिस्टम का एक औपचारिक (गणितीय) मॉडल विकसित करता है। फिर हम अनुबंध के मॉडल और उसके विनिर्देश के बीच स्थिरता की जांच करने के लिए एक औपचारिक प्रमाण प्रक्रिया का पालन कर सकते हैं।

औपचारिक सत्यापन के साथ, यह सत्यापित करने का प्रश्न कि क्या अनुबंध का व्यावसायिक तर्क आवश्यकताओं को पूरा करता है, एक गणितीय प्रस्ताव है जिसे साबित या अस्वीकृत किया जा सकता है। औपचारिक रूप से एक प्रस्ताव साबित करके, हम सीमित संख्या में चरणों के साथ अनंत संख्या में परीक्षण मामलों को सत्यापित कर सकते हैं। इस तरह औपचारिक सत्यापन में यह साबित करने की बेहतर संभावनाएं हैं कि एक अनुबंध विनिर्देश के संबंध में कार्यात्मक रूप से सही है।

आदर्श सत्यापन लक्ष्य

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

स्मार्ट अनुबंध—कम से कम, कुछ हद तक—दोनों आवश्यकताओं को पूरा करते हैं। उदाहरण के लिए, इथेरियम अनुबंधों का छोटा आकार उन्हें औपचारिक सत्यापन के लिए उत्तरदायी बनाता है। इसी तरह, EVM सरल नियमों का पालन करता है, जो EVM में चलने वाले प्रोग्रामों के लिए अर्थपूर्ण गुणों को निर्दिष्ट करना और सत्यापित करना आसान बनाता है।

तेज़ विकास चक्र

औपचारिक सत्यापन तकनीकें, जैसे मॉडल चेकिंग और प्रतीकात्मक निष्पादन, आम तौर पर स्मार्ट अनुबंध कोड के नियमित विश्लेषण (परीक्षण या ऑडिटिंग के दौरान किए गए) की तुलना में अधिक कुशल होती हैं। ऐसा इसलिए है क्योंकि औपचारिक सत्यापन दावों का परीक्षण करने के लिए प्रतीकात्मक मानों पर निर्भर करता है ("क्या होगा यदि कोई उपयोगकर्ता n ईथर निकालने का प्रयास करता है?") परीक्षण के विपरीत जो ठोस मानों का उपयोग करता है ("क्या होगा यदि कोई उपयोगकर्ता 5 ईथर निकालने का प्रयास करता है?")।

प्रतीकात्मक इनपुट चर ठोस मानों के कई वर्गों को कवर कर सकते हैं, इसलिए औपचारिक सत्यापन दृष्टिकोण कम समय सीमा में अधिक कोड कवरेज का वादा करते हैं। जब प्रभावी ढंग से उपयोग किया जाता है, तो औपचारिक सत्यापन डेवलपर्स के लिए विकास चक्र को तेज कर सकता है।

औपचारिक सत्यापन महंगी डिज़ाइन त्रुटियों को कम करके विकेंद्रीकृत एप्लिकेशन (dapp) बनाने की प्रक्रिया में भी सुधार करता है। कमजोरियों को ठीक करने के लिए अनुबंधों को अपग्रेड करने (जहां संभव हो) के लिए कोडबेस के व्यापक पुनर्लेखन और विकास पर अधिक प्रयास खर्च करने की आवश्यकता होती है। औपचारिक सत्यापन अनुबंध कार्यान्वयन में कई त्रुटियों का पता लगा सकता है जो परीक्षकों और ऑडिटर्स से बच सकती हैं और अनुबंध को तैनात करने से पहले उन मुद्दों को ठीक करने का पर्याप्त अवसर प्रदान करता है।

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

शारीरिक श्रम की लागत

औपचारिक सत्यापन, विशेष रूप से अर्ध-स्वचालित सत्यापन जिसमें एक इंसान शुद्धता प्रमाण प्राप्त करने के लिए प्रमाणक का मार्गदर्शन करता है, के लिए काफी शारीरिक श्रम की आवश्यकता होती है। इसके अलावा, औपचारिक विनिर्देश बनाना एक जटिल गतिविधि है जिसके लिए उच्च स्तर के कौशल की आवश्यकता होती है।

ये कारक (प्रयास और कौशल) अनुबंधों में शुद्धता का आकलन करने के सामान्य तरीकों, जैसे परीक्षण और ऑडिट की तुलना में औपचारिक सत्यापन को अधिक मांग वाला और महंगा बनाते हैं। फिर भी, स्मार्ट अनुबंध कार्यान्वयन में त्रुटियों की लागत को देखते हुए, पूर्ण सत्यापन ऑडिट के लिए लागत का भुगतान करना व्यावहारिक है।

गलत नकारात्मक

औपचारिक सत्यापन केवल यह जांच सकता है कि क्या स्मार्ट अनुबंध का निष्पादन औपचारिक विनिर्देश से मेल खाता है। इस प्रकार, यह सुनिश्चित करना महत्वपूर्ण है कि विनिर्देश स्मार्ट अनुबंध के अपेक्षित व्यवहारों का ठीक से वर्णन करता है।

यदि विनिर्देश खराब तरीके से लिखे गए हैं, तो संपत्तियों के उल्लंघन—जो कमजोर निष्पादन की ओर इशारा करते हैं—का औपचारिक सत्यापन ऑडिट द्वारा पता नहीं लगाया जा सकता है। इस मामले में, एक डेवलपर गलती से यह मान सकता है कि अनुबंध बग-मुक्त है।

प्रदर्शन संबंधी समस्याएं

औपचारिक सत्यापन कई प्रदर्शन संबंधी समस्याओं में चलता है। उदाहरण के लिए, क्रमशः मॉडल चेकिंग और प्रतीकात्मक चेकिंग के दौरान आने वाली स्थिति और पथ विस्फोट समस्याएं सत्यापन प्रक्रियाओं को प्रभावित कर सकती हैं। इसके अलावा, औपचारिक सत्यापन उपकरण अक्सर अपनी अंतर्निहित परत में SMT समाधानकर्ताओं और अन्य बाधा समाधानकर्ताओं का उपयोग करते हैं, और ये समाधानकर्ता कम्प्यूटेशनल रूप से गहन प्रक्रियाओं पर निर्भर करते हैं।

इसके अलावा, प्रोग्राम सत्यापनकर्ताओं के लिए यह निर्धारित करना हमेशा संभव नहीं होता है कि क्या कोई संपत्ति (तार्किक सूत्र के रूप में वर्णित) संतुष्ट हो सकती है या नहीं ("निर्णय क्षमता की समस्या (opens in a new tab)") क्योंकि एक प्रोग्राम कभी समाप्त नहीं हो सकता है। इस प्रकार, किसी अनुबंध के लिए कुछ गुणों को साबित करना असंभव हो सकता है, भले ही वह अच्छी तरह से निर्दिष्ट हो।

इथेरियम स्मार्ट अनुबंधों के लिए औपचारिक सत्यापन उपकरण

औपचारिक विनिर्देश बनाने के लिए विनिर्देश भाषाएं

Act: Act स्टोरेज अपडेट, पूर्व/पश्च शर्तों और अनुबंध इनवेरिएंट्स के विनिर्देश की अनुमति देता है। इसके टूल सूट में Coq, SMT समाधानकर्ताओं, या hevm के माध्यम से कई गुणों को साबित करने में सक्षम प्रूफ बैकएंड भी हैं।

Scribble - Scribble विनिर्देश भाषा में कोड एनोटेशन को ठोस दावों में बदल देता है जो विनिर्देश की जांच करते हैं।

दस्तावेज़ीकरण (opens in a new tab)

Dafny - Dafny एक सत्यापन-तैयार प्रोग्रामिंग भाषा है जो कोड की शुद्धता के बारे में तर्क करने और साबित करने के लिए उच्च-स्तरीय एनोटेशन पर निर्भर करती है।

GitHub (opens in a new tab)

शुद्धता की जांच के लिए प्रोग्राम सत्यापनकर्ता

Certora Prover - Certora Prover स्मार्ट अनुबंधों में कोड की शुद्धता की जांच के लिए एक स्वचालित औपचारिक सत्यापन उपकरण है। विनिर्देश CVL (Certora Verification Language) में लिखे गए हैं, जिसमें स्थिर विश्लेषण और बाधा-समाधान के संयोजन का उपयोग करके संपत्ति के उल्लंघन का पता लगाया जाता है।

Solidity SMTChecker - Solidity का SMTChecker SMT (Satisfiability Modulo Theories) और Horn सॉल्विंग पर आधारित एक अंतर्निहित मॉडल चेकर है। यह पुष्टि करता है कि क्या संकलन के दौरान अनुबंध का स्रोत कोड विनिर्देशों से मेल खाता है और सुरक्षा गुणों के उल्लंघन के लिए स्थिर रूप से जांच करता है।

GitHub (opens in a new tab)

solc-verify - solc-verify Solidity कंपाइलर का एक विस्तारित संस्करण है जो एनोटेशन और मॉड्यूलर प्रोग्राम सत्यापन का उपयोग करके Solidity कोड पर स्वचालित औपचारिक सत्यापन कर सकता है।

GitHub (opens in a new tab)

KEVM - KEVM K फ्रेमवर्क में लिखा गया इथेरियम वर्चुअल मशीन (EVM) का एक औपचारिक शब्दार्थ है। KEVM निष्पादन योग्य है और रीचेबिलिटी लॉजिक का उपयोग करके कुछ संपत्ति-संबंधित दावों को साबित कर सकता है।

प्रमेय सिद्ध करने के लिए तार्किक फ्रेमवर्क

Isabelle - Isabelle/HOL एक प्रमाण सहायक है जो गणितीय सूत्रों को एक औपचारिक भाषा में व्यक्त करने की अनुमति देता है और उन सूत्रों को साबित करने के लिए उपकरण प्रदान करता है। मुख्य अनुप्रयोग गणितीय प्रमाणों का औपचारिकरण है और विशेष रूप से औपचारिक सत्यापन, जिसमें कंप्यूटर हार्डवेयर या सॉफ़्टवेयर की शुद्धता साबित करना और कंप्यूटर भाषाओं और प्रोटोकॉल के गुणों को साबित करना शामिल है।

Rocq - Rocq एक संवादात्मक प्रमेय प्रमाणक है जो आपको प्रमेयों का उपयोग करके प्रोग्रामों को परिभाषित करने और अंतःक्रियात्मक रूप से शुद्धता के मशीन-जांच किए गए प्रमाण उत्पन्न करने देता है।

स्मार्ट अनुबंधों में कमजोर पैटर्न का पता लगाने के लिए प्रतीकात्मक निष्पादन-आधारित उपकरण

मैन्टिकोर - प्रतीकात्मक निष्पादन के आधार पर EVM बाइटकोड विश्लेषण उपकरण का विश्लेषण करने के लिए एक उपकरण।

hevm - hevm EVM बाइटकोड के लिए एक प्रतीकात्मक निष्पादन इंजन और तुल्यता चेकर है।

GitHub (opens in a new tab)

Mythril - इथेरियम स्मार्ट अनुबंधों में कमजोरियों का पता लगाने के लिए एक प्रतीकात्मक निष्पादन उपकरण