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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

औपचारिक विनिर्देश प्रोग्राम लॉजिक(opens in a new tab) के तत्वों का उपयोग करके प्राप्त किए जाते हैं, जो किसी प्रोग्राम के गुणों के बारे में औपचारिक तर्क की अनुमति देते हैं। एक प्रोग्राम लॉजिक में औपचारिक नियम होते हैं जो किसी प्रोग्राम के अपेक्षित व्यवहार (गणितीय भाषा में) के बारे में बताते हैं। औपचारिक विनिर्देशों को बनाने में विभिन्न प्रोग्राम लॉजिक्स का उपयोग किया जाता है, जिसमें रीचेबिलिटी लॉजिक(opens in a new tab), टेम्पोरल लॉजिक(opens in a new tab) और होरे लॉजिक(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() का उपयोग करने की शर्तों को कवर करती है: “प्रेषक की शेष राशि कभी भी भेजे जाने वाले टोकन की अनुरोधित राशि से कम नहीं होती है।”। एक अनुबंध अपरिवर्तनीय के इस प्राकृतिक-भाषा विवरण को एक औपचारिक (गणितीय) विनिर्देश में अनुवादित किया जा सकता है, जिसे तब वैधता के लिए कड़ाई से जांचा जा सकता है।

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

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

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

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

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

होरे-शैली के गुण

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

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

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

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

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

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

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

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

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

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

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

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

धनराशि जमा करें
धन जमा करने के बाद प्रस्ताव पर मतदान करें
अगर वे किसी प्रस्ताव पर मतदान नहीं करते हैं, तो धनवापसी का दावा करें

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

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

मॉडल जाँच

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

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

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

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

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

प्रमेय साबित करना

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

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

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

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

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

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

प्रतीकात्मक निष्पादन कॉन्क्रीट मानों (जैसे, 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 का उत्पादन कर सकता है।

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

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

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

1function safe_add(uint x, uint y) returns(uint z){
2
3  z = x + y;
4  require(z>=x);
5  require(z>=y);
6
7  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 ईथर वापस लेने की कोशिश करता है?")।

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

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

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

मैन्युअल श्रम की लागत

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

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

झूठी नकारात्मकता

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

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

परफ़ॉर्मेंस से जुड़ी समस्याएँ

औपचारिक सत्यापन परफ़ॉर्मेंस से जुड़ी कई समस्याओं में चलता है। उदाहरण के लिए, मॉडल जाँच और प्रतीकात्मक जाँच के दौरान खासकर राज्य और पथ विस्फोट की समस्याएँ सत्यापन प्रक्रियाओं को प्रभावित कर सकती हैं। इसके अलावा, औपचारिक सत्यापन उपकरण अक्सर अपनी अंतर्निहित परत में 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 (सर्टोसा वेरिफिकेशन लैंग्वेज) में लिखे गए हैं, जिसमें स्थिर विश्लेषण और बाधा-समाधान के संयोजन का उपयोग करके विशेषता के उल्लंघन का पता लगाया गया है।

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

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

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

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

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

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

गिटहब(opens in a new tab)

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