स्मार्ट कॉन्ट्रॅक्ट्सची औपचारिक पडताळणी

स्मार्ट कॉन्ट्रॅक्ट्स विकेंद्रित, विश्वासहीन आणि मजबूत ॲप्लिकेशन्स तयार करणे शक्य करत आहेत जे नवीन उपयोग-प्रकरणे सादर करतात आणि वापरकर्त्यांसाठी मूल्य अनलॉक करतात. कारण स्मार्ट कॉन्ट्रॅक्ट्स मोठ्या प्रमाणात मूल्य हाताळतात, त्यामुळे डेव्हलपर्ससाठी सुरक्षा हा एक महत्त्वपूर्ण विचार आहे.

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

स्मार्ट कॉन्ट्रॅक्ट्समध्ये लागू केल्यावर, औपचारिक पडताळणी हे सिद्ध करू शकते की कॉन्ट्रॅक्टचा व्यावसायिक तर्क पूर्वनिर्धारित विनिर्देशनाची पूर्तता करतो. कॉन्ट्रॅक्ट कोडच्या अचूकतेचे मूल्यांकन करण्याच्या इतर पद्धतींच्या तुलनेत, जसे की चाचणी, औपचारिक पडताळणी स्मार्ट कॉन्ट्रॅक्ट कार्यात्मकदृष्ट्या योग्य असल्याची अधिक मजबूत हमी देते.

औपचारिक पडताळणी म्हणजे काय?

औपचारिक पडताळणी म्हणजे औपचारिक विनिर्देशनाच्या संदर्भात प्रणालीच्या अचूकतेचे मूल्यांकन करण्याची प्रक्रिया. सोप्या भाषेत सांगायचे तर, औपचारिक पडताळणी आपल्याला हे तपासण्याची परवानगी देते की प्रणालीचे वर्तन काही आवश्यकतांची पूर्तता करते की नाही (म्हणजेच, ते आपल्याला हवे ते करते).

प्रणालीचे (या प्रकरणात स्मार्ट कॉन्ट्रॅक्ट) अपेक्षित वर्तन औपचारिक मॉडेलिंग वापरून वर्णन केले जाते, तर विनिर्देशन भाषा औपचारिक गुणधर्म तयार करण्यास सक्षम करतात. औपचारिक पडताळणी तंत्रे नंतर हे सत्यापित करू शकतात की कॉन्ट्रॅक्टची अंमलबजावणी त्याच्या विनिर्देशनाचे पालन करते आणि पूर्वीच्या अचूकतेचा गणितीय पुरावा मिळवू शकतात. जेव्हा एखादा कॉन्ट्रॅक्ट त्याच्या विनिर्देशनाची पूर्तता करतो, तेव्हा त्याचे वर्णन “कार्यात्मकदृष्ट्या योग्य”, “डिझाइननुसार योग्य” किंवा “बांधणीनुसार योग्य” असे केले जाते.

औपचारिक मॉडेल म्हणजे काय?

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

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

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

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

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

निम्न-स्तरीय मॉडेल्स आदर्श मानले जातात कारण ते Ethereum च्या अंमलबजावणी वातावरणात (म्हणजेच, 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 (म्हणजेच, प्रोग्राम) च्या स्थितीवरील प्रेडिकेट्स आहेत, ज्यांना अनुक्रमे पूर्वअटी आणि उत्तरअटी म्हणून औपचारिकपणे वर्णन केले जाते.

पूर्वअट ही एक प्रेडिकेट आहे जी फंक्शनच्या योग्य अंमलबजावणीसाठी आवश्यक असलेल्या अटींचे वर्णन करते; कॉन्ट्रॅक्टमध्ये कॉल करणाऱ्या वापरकर्त्यांनी ही आवश्यकता पूर्ण केली पाहिजे. उत्तरअट ही एक प्रेडिकेट आहे जी फंक्शन योग्यरित्या कार्यान्वित झाल्यास स्थापित होणारी स्थिती दर्शवते; फंक्शन कॉल केल्यानंतर वापरकर्ते ही स्थिती खरी होण्याची अपेक्षा करू शकतात. होअर लॉजिकमधील एक अचल (invariant) एक प्रेडिकेट आहे जे फंक्शनच्या अंमलबजावणीद्वारे संरक्षित केले जाते (म्हणजेच ते बदलत नाही).

होअर-शैलीतील विनिर्देशने आंशिक अचूकता किंवा संपूर्ण अचूकता यांची हमी देऊ शकतात. कॉन्ट्रॅक्ट फंक्शनची अंमलबजावणी "आंशिकपणे योग्य" असते जर फंक्शन कार्यान्वित होण्यापूर्वी पूर्वअट खरी असेल आणि अंमलबजावणी समाप्त झाल्यास, उत्तरअट देखील खरी असते. जर फंक्शन कार्यान्वित होण्यापूर्वी पूर्वअट खरी असेल, अंमलबजावणी समाप्त होण्याची हमी असेल आणि ती समाप्त झाल्यावर उत्तरअट खरी असेल तर संपूर्ण अचूकतेचा पुरावा मिळतो.

संपूर्ण अचूकतेचा पुरावा मिळवणे कठीण आहे कारण काही अंमलबजावणी समाप्त होण्यापूर्वी विलंब होऊ शकतात, किंवा कधीही समाप्त होत नाहीत. तरीही, अंमलबजावणी समाप्त होते की नाही हा प्रश्न विवादास्पद आहे कारण Ethereum ची गॅस यंत्रणा अनंत प्रोग्राम लूप्सना प्रतिबंधित करते (अंमलबजावणी एकतर यशस्वीरित्या समाप्त होते किंवा 'आउट-ऑफ-गॅस' त्रुटीमुळे संपते).

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

अनेक औपचारिक पडताळणी फ्रेमवर्क फंक्शन्सच्या अर्थपूर्ण अचूकतेचा पुरावा देण्यासाठी होअर-शैलीतील विनिर्देशनांचा वापर करतात. Solidity मध्ये require आणि assert विधानांचा वापर करून होअर-शैलीतील गुणधर्म (प्रतिपादने म्हणून) थेट कॉन्ट्रॅक्ट कोडमध्ये जोडणे देखील शक्य आहे.

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 तयार करू शकतो.

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

शिवाय, प्रतीकात्मक अंमलबजावणी इतर गुणधर्म-आधारित तंत्रांपेक्षा (उदा., फझिंग) कमी चुकीचे सकारात्मक परिणाम देते जे फंक्शनला यादृच्छिकपणे इनपुट तयार करतात. जर प्रतीकात्मक अंमलबजावणी दरम्यान त्रुटीची स्थिती ट्रिगर झाली, तर त्रुटी ट्रिगर करणारे ठोस मूल्य तयार करणे आणि समस्येचे पुनरुत्पादन करणे शक्य आहे.

प्रतीकात्मक अंमलबजावणी अचूकतेचा काही प्रमाणात गणितीय पुरावा देखील देऊ शकते. ओव्हरफ्लो संरक्षणासह कॉन्ट्रॅक्ट फंक्शनचे खालील उदाहरण विचारात घ्या:

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). तथापि, उपयोजनापूर्वी कॉन्ट्रॅक्टची औपचारिक पडताळणी केल्याने, ब्लॉकचेनवर चालल्यावर ते अपेक्षेप्रमाणे कार्य करेल याची हमी वाढू शकते.

कोणत्याही स्मार्ट कॉन्ट्रॅक्टमध्ये विश्वसनीयता हा अत्यंत इष्ट गुण आहे, विशेषतः कारण Ethereum व्हर्च्युअल मशीन (EVM) मध्ये तैनात केलेला कोड सामान्यतः अपरिवर्तनीय असतो. लॉन्च-नंतरचे अपग्रेड सहज उपलब्ध नसल्यामुळे, कॉन्ट्रॅक्ट्सच्या विश्वसनीयतेची हमी देण्याची गरज औपचारिक पडताळणी आवश्यक करते. औपचारिक पडताळणी इंटीजर अंडरफ्लो आणि ओव्हरफ्लो, री-एन्ट्रन्सी आणि खराब गॅस ऑप्टिमायझेशन यांसारख्या अवघड समस्या शोधू शकते, ज्या ऑडिटर्स आणि टेस्टर्सकडून सुटू शकतात.

कार्यात्मक अचूकता सिद्ध करा

स्मार्ट कॉन्ट्रॅक्ट काही आवश्यकता पूर्ण करतो हे सिद्ध करण्याची सर्वात सामान्य पद्धत प्रोग्राम चाचणी आहे. यामध्ये कॉन्ट्रॅक्टला अपेक्षित असलेल्या डेटाच्या नमुन्यासह कार्यान्वित करणे आणि त्याच्या वर्तनाचे विश्लेषण करणे समाविष्ट आहे. जर कॉन्ट्रॅक्ट नमुना डेटासाठी अपेक्षित परिणाम देत असेल, तर डेव्हलपर्सकडे त्याच्या अचूकतेचा वस्तुनिष्ठ पुरावा असतो.

तथापि, हा दृष्टिकोन नमुन्याचा भाग नसलेल्या इनपुट मूल्यांसाठी योग्य अंमलबजावणी सिद्ध करू शकत नाही. म्हणून, कॉन्ट्रॅक्टची चाचणी बग शोधण्यात मदत करू शकते (म्हणजे, अंमलबजावणी दरम्यान काही कोड पाथ इच्छित परिणाम देत नसतील तर), पण ते बगच्या अनुपस्थितीचा निर्णायक पुरावा देऊ शकत नाही.

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

औपचारिक पडताळणीसह, कॉन्ट्रॅक्टचा व्यावसायिक तर्क आवश्यकता पूर्ण करतो की नाही हे सत्यापित करण्याचा प्रश्न एक गणितीय प्रस्ताव आहे जो सिद्ध किंवा असिद्ध केला जाऊ शकतो. औपचारिकपणे प्रस्ताव सिद्ध करून, आम्ही मर्यादित संख्येच्या चरणांसह अनंत संख्येच्या चाचणी प्रकरणांची पडताळणी करू शकतो. या प्रकारे औपचारिक पडताळणीला विनिर्देशनाच्या संदर्भात कॉन्ट्रॅक्ट कार्यात्मकदृष्ट्या योग्य आहे हे सिद्ध करण्याची चांगली शक्यता असते.

आदर्श पडताळणी लक्ष्ये

पडताळणी लक्ष्य औपचारिकपणे सत्यापित करायच्या प्रणालीचे वर्णन करते. औपचारिक पडताळणीचा वापर "एम्बेडेड सिस्टम्स" मध्ये सर्वोत्तम होतो (मोठ्या प्रणालीचा भाग असलेले लहान, साधे सॉफ्टवेअरचे तुकडे). ते विशेष डोमेनसाठी देखील आदर्श आहेत ज्यात कमी नियम आहेत, कारण यामुळे डोमेन-विशिष्ट गुणधर्मांची पडताळणी करण्यासाठी साधने सुधारणे सोपे होते.

स्मार्ट कॉन्ट्रॅक्ट्स—किमान, काही प्रमाणात—दोन्ही आवश्यकता पूर्ण करतात. उदाहरणार्थ, Ethereum कॉन्ट्रॅक्ट्सचा लहान आकार त्यांना औपचारिक पडताळणीसाठी अनुकूल बनवतो. त्याचप्रमाणे, EVM सोप्या नियमांचे पालन करते, ज्यामुळे EVM मध्ये चालणाऱ्या प्रोग्राम्ससाठी सिमेंटिक गुणधर्म निर्दिष्ट करणे आणि सत्यापित करणे सोपे होते.

जलद विकास चक्र

मॉडेल तपासणी आणि प्रतीकात्मक अंमलबजावणी यांसारखी औपचारिक पडताळणी तंत्रे साधारणपणे स्मार्ट कॉन्ट्रॅक्ट कोडच्या नियमित विश्लेषणापेक्षा (चाचणी किंवा ऑडिटिंग दरम्यान केल्या जाणाऱ्या) अधिक कार्यक्षम असतात. याचे कारण असे की औपचारिक पडताळणी प्रतिपादनांची चाचणी घेण्यासाठी प्रतीकात्मक मूल्यांवर अवलंबून असते ("जर वापरकर्त्याने n ईथर काढण्याचा प्रयत्न केला तर काय होईल?"). चाचणीच्या विपरीत जी ठोस मूल्ये वापरते ("जर वापरकर्त्याने 5 ईथर काढण्याचा प्रयत्न केला तर काय होईल?").

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

औपचारिक पडताळणी खर्चिक डिझाइन त्रुटी कमी करून विकेंद्रित ॲप्लिकेशन्स (dapps) तयार करण्याची प्रक्रिया सुधारते. असुरक्षितता दूर करण्यासाठी कॉन्ट्रॅक्ट्स अपग्रेड करण्यासाठी (जेथे शक्य असेल) कोडबेसचे विस्तृत पुनर्लेखन आणि विकासावर अधिक प्रयत्न आवश्यक आहेत. औपचारिक पडताळणी कॉन्ट्रॅक्ट अंमलबजावणीमधील अनेक त्रुटी शोधू शकते ज्या टेस्टर्स आणि ऑडिटर्सकडून सुटू शकतात आणि कॉन्ट्रॅक्ट तैनात करण्यापूर्वी त्या समस्या दूर करण्याची पुरेशी संधी देते.

औपचारिक पडताळणीचे तोटे

मॅन्युअल श्रमाचा खर्च

औपचारिक पडताळणी, विशेषतः अर्ध-स्वयंचलित पडताळणी ज्यात मानव प्रोव्हरला अचूकतेचे पुरावे मिळवण्यासाठी मार्गदर्शन करतो, त्यासाठी मोठ्या प्रमाणात मॅन्युअल श्रम आवश्यक आहेत. शिवाय, औपचारिक विनिर्देशन तयार करणे ही एक जटिल क्रिया आहे ज्यासाठी उच्च पातळीचे कौशल्य आवश्यक आहे.

हे घटक (प्रयत्न आणि कौशल्य) औपचारिक पडताळणीला कॉन्ट्रॅक्ट्समधील अचूकतेचे मूल्यांकन करण्याच्या नेहमीच्या पद्धतींपेक्षा, जसे की चाचणी आणि ऑडिट, अधिक मागणीपूर्ण आणि महाग बनवतात. तरीही, स्मार्ट कॉन्ट्रॅक्ट अंमलबजावणीतील त्रुटींचा खर्च पाहता, पूर्ण पडताळणी ऑडिटसाठी खर्च करणे व्यावहारिक आहे.

खोटे नकारात्मक

औपचारिक पडताळणी केवळ स्मार्ट कॉन्ट्रॅक्टची अंमलबजावणी औपचारिक विनिर्देशनाशी जुळते की नाही हे तपासू शकते. त्यामुळे, विनिर्देशन स्मार्ट कॉन्ट्रॅक्टच्या अपेक्षित वर्तनांचे योग्यरित्या वर्णन करते याची खात्री करणे महत्त्वाचे आहे.

जर विनिर्देशने खराब लिहिलेली असतील, तर गुणधर्मांचे उल्लंघन—जे असुरक्षित अंमलबजावणीकडे निर्देश करतात—औपचारिक पडताळणी ऑडिटद्वारे शोधले जाऊ शकत नाहीत. या प्रकरणात, डेव्हलपर चुकीने समजू शकतो की कॉन्ट्रॅक्ट बग-मुक्त आहे.

कार्यप्रदर्शन समस्या

औपचारिक पडताळणीमध्ये अनेक कार्यप्रदर्शन समस्या येतात. उदाहरणार्थ, मॉडेल तपासणी आणि प्रतीकात्मक तपासणी दरम्यान अनुक्रमे येणाऱ्या स्टेट आणि पाथ एक्सप्लोजन समस्या पडताळणी प्रक्रियांना प्रभावित करू शकतात. तसेच, औपचारिक पडताळणी साधने अनेकदा त्यांच्या अंतर्निहित स्तरावर SMT सॉल्व्हर्स आणि इतर कंस्ट्रेंट सॉल्व्हर्स वापरतात, आणि हे सॉल्व्हर्स संगणकीयदृष्ट्या गहन प्रक्रियांवर अवलंबून असतात.

तसेच, प्रोग्राम व्हेरिफायर्सना नेहमीच हे ठरवणे शक्य नसते की एखादा गुणधर्म (लॉजिकल फॉर्म्युला म्हणून वर्णन केलेला) पूर्ण केला जाऊ शकतो की नाही (the "decidability problem (opens in a new tab)") कारण प्रोग्राम कधीही समाप्त होऊ शकत नाही. त्यामुळे, कॉन्ट्रॅक्ट व्यवस्थित निर्दिष्ट केलेला असला तरीही काही गुणधर्म सिद्ध करणे अशक्य असू शकते.

Ethereum स्मार्ट कॉन्ट्रॅक्ट्ससाठी औपचारिक पडताळणी साधने

औपचारिक विनिर्देशने तयार करण्यासाठी विनिर्देशन भाषा

Act: Act स्टोरेज अद्यतने, पूर्व/उत्तर अटी आणि कॉन्ट्रॅक्ट अचलांचे विनिर्देशन करण्याची परवानगी देते. त्याच्या टूल सूटमध्ये पुरावा बॅकएंड्स देखील आहेत जे Coq, SMT सॉल्व्हर्स किंवा hevm द्वारे अनेक गुणधर्म सिद्ध करण्यास सक्षम आहेत.

Scribble - Scribble, Scribble विनिर्देशन भाषेतील कोड भाष्यांना ठोस प्रतिपादनांमध्ये रूपांतरित करते जे विनिर्देशन तपासतात.

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

Dafny - Dafny ही पडताळणी-तयार प्रोग्रामिंग भाषा आहे जी कोडच्या अचूकतेबद्दल तर्क करण्यासाठी आणि सिद्ध करण्यासाठी उच्च-स्तरीय भाष्यांवर अवलंबून असते.

GitHub (opens in a new tab)

अचूकता तपासण्यासाठी प्रोग्राम व्हेरिफायर्स

Certora Prover - Certora Prover हे स्मार्ट कॉन्ट्रॅक्ट्समधील कोडची अचूकता तपासण्यासाठी एक स्वयंचलित औपचारिक पडताळणी साधन आहे. विनिर्देशने CVL (Certora व्हेरिफिकेशन लँग्वेज) मध्ये लिहिली जातात, ज्यात स्टॅटिक विश्लेषण आणि कंस्ट्रेंट-सॉल्व्हिंगच्या संयोगाने गुणधर्म उल्लंघने शोधली जातात.

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 फ्रेमवर्कमध्ये लिहिलेले Ethereum व्हर्च्युअल मशीन (EVM) चे औपचारिक सिमेंटिक्स आहे. KEVM कार्यान्वित करण्यायोग्य आहे आणि रीचेबिलिटी लॉजिक वापरून काही गुणधर्म-संबंधित प्रतिपादने सिद्ध करू शकते.

प्रमेय सिद्ध करण्यासाठी तार्किक फ्रेमवर्क

Isabelle - Isabelle/HOL एक पुरावा सहाय्यक आहे जो गणितीय सूत्रांना औपचारिक भाषेत व्यक्त करण्याची परवानगी देतो आणि ती सूत्रे सिद्ध करण्यासाठी साधने प्रदान करतो. मुख्य ॲप्लिकेशन गणितीय पुराव्यांचे औपचारिकीकरण आणि विशेषतः औपचारिक पडताळणी आहे, ज्यात संगणक हार्डवेअर किंवा सॉफ्टवेअरची अचूकता सिद्ध करणे आणि संगणक भाषा आणि प्रोटोकॉलचे गुणधर्म सिद्ध करणे समाविष्ट आहे.

Rocq - Rocq एक इंटरॅक्टिव्ह प्रमेय प्रोव्हर आहे जो तुम्हाला प्रमेयांचा वापर करून प्रोग्राम्स परिभाषित करू देतो आणि अचूकतेचे मशीन-चेक्ड पुरावे इंटरॅक्टिव्हपणे तयार करू देतो.

स्मार्ट कॉन्ट्रॅक्ट्समध्ये असुरक्षित नमुने शोधण्यासाठी प्रतीकात्मक अंमलबजावणी-आधारित साधने

Manticore - प्रतीकात्मक अंमलबजावणीवर आधारित EVM बायकोड विश्लेषणासाठी एक साधन.

hevm - hevm हे EVM बायकोडसाठी एक प्रतीकात्मक अंमलबजावणी इंजिन आणि समतुल्यता तपासक आहे.

GitHub (opens in a new tab)

Mythril - Ethereum स्मार्ट कॉन्ट्रॅक्ट्समधील असुरक्षितता शोधण्यासाठी एक प्रतीकात्मक अंमलबजावणी साधन