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

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

औपचारिक सत्यापन स्मार्ट अनुबंध सुरक्षा में सुधार के लिए सुझाई गई तकनीकों में से एक है। औपचारिक सत्यापन, जो प्रोग्रामों को निर्दिष्ट करने, डिजाइन करने और सत्यापित करने के लिए औपचारिक तरीकों (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) के रूप में मॉडल करते हैं, जो संचालन करके स्थितियों (states) के बीच ट्रांज़िशन कर सकता है, और 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 (यानी, प्रोग्राम) की स्टेट पर विधेय (predicates) हैं, जिन्हें औपचारिक रूप से क्रमशः प्रीकंडीशंस और पोस्टकंडीशंस के रूप में वर्णित किया गया है।

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

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

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

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

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

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

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

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

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

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

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

• धनराशि जमा करें

• धन जमा करने के बाद प्रस्ताव पर मतदान करें

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

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

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

मॉडल चेकिंग

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

मॉडल चेकिंग के लिए एक सिस्टम (यानी, एक अनुबंध) का एक अमूर्त गणितीय निरूपण बनाने और प्रस्तावात्मक तर्क (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 उत्पन्न कर सकता है।

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

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

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

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;
8}

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

• गिटहब (opens in a new tab)
• प्रलेखन (opens in a new tab)

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

• प्रलेखन (opens in a new tab)

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

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

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

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

• वेबसाइट (opens in a new tab)
• प्रलेखन (opens in a new tab)

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

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

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

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

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

• गिटहब (opens in a new tab)
• प्रलेखन (opens in a new tab)

थ्योरम प्रूविंग के लिए तार्किक ढाँचे

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

• गिटहब (opens in a new tab)
• प्रलेखन (opens in a new tab)

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

• गिटहब (opens in a new tab)
• प्रलेखन (opens in a new tab)

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

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

• गिटहब (opens in a new tab)
• प्रलेखन (opens in a new tab)

hevm - hevm एक सिंबॉलिक निष्पादन इंजन और 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)
• एथेरियम इकोसिस्टम में औपचारिक सत्यापन परियोजनाओं का अवलोकन (opens in a new tab)
• एथेरियम 2.0 डिपॉजिट स्मार्ट अनुबंध का एंड-टू-एंड औपचारिक सत्यापन (opens in a new tab)
• दुनिया के सबसे लोकप्रिय स्मार्ट अनुबंध का औपचारिक रूप से सत्यापन (opens in a new tab)
• SMTChecker और औपचारिक सत्यापन (opens in a new tab)