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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

स्मार्ट कॉन्ट्रॅक्ट्सच्या संदर्भात, औपचारिक तपशील म्हणजे गुणधर्म—कॉन्ट्रॅक्टने पूर्ण केल्या पाहिजेत अशा आवश्यकतांचे औपचारिक वर्णन. अशा गुणधर्मांचे वर्णन "इनव्हेरियंट्स" (invariants) म्हणून केले जाते आणि ते कॉन्ट्रॅक्टच्या अंमलबजावणीबद्दल तार्किक दृढकथनांचे प्रतिनिधित्व करतात जे कोणत्याही अपवादाशिवाय, प्रत्येक संभाव्य परिस्थितीत सत्य राहिले पाहिजेत.

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

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

स्मार्ट कॉन्ट्रॅक्ट्ससाठी औपचारिक तपशीलांचे प्रकार

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

औपचारिक तपशील प्रोग्राम लॉजिकच्या (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) म्हणून मॉडेल करतात, जे ऑपरेशन्स करून स्थितींमध्ये (states) संक्रमण करू शकते, ज्यामध्ये FSM मॉडेलसाठी औपचारिक गुणधर्म परिभाषित करण्यासाठी टेम्पोरल लॉजिक वापरले जाते.

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

उच्च-स्तरीय तपशील सामान्यतः स्मार्ट कॉन्ट्रॅक्ट्ससाठी दोन महत्त्वपूर्ण टेम्पोरल गुणधर्म कॅप्चर करतात: सुरक्षा (safety) आणि लाइव्हनेस (liveness). सुरक्षा गुणधर्म "कधीही काहीही वाईट घडत नाही" या कल्पनेचे प्रतिनिधित्व करतात आणि सहसा इनव्हेरियन्स व्यक्त करतात. सुरक्षा गुणधर्म सामान्य सॉफ्टवेअर आवश्यकता परिभाषित करू शकतो, जसे की डेडॉक (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 कॉल करू शकतो) औपचारिक लॉजिकमध्ये लिहिला जाऊ शकतो. त्यानंतर, मॉडेल-चेकिंग अल्गोरिदम कॉन्ट्रॅक्ट या औपचारिक तपशीलाची पूर्तता करते की नाही हे पडताळून पाहू शकतो.

मॉडेल चेकिंग स्टेट स्पेस एक्सप्लोरेशन वापरते, ज्यामध्ये स्मार्ट कॉन्ट्रॅक्टच्या सर्व संभाव्य स्थिती तयार करणे आणि गुणधर्मांचे उल्लंघन करणाऱ्या पोहोचण्यायोग्य स्थिती शोधण्याचा प्रयत्न करणे समाविष्ट आहे. तथापि, यामुळे अनंत संख्येने स्थिती निर्माण होऊ शकतात (ज्याला "स्टेट एक्सप्लोजन प्रॉब्लेम" म्हणून ओळखले जाते), म्हणून मॉडेल चेकर्स स्मार्ट कॉन्ट्रॅक्ट्सचे कार्यक्षम विश्लेषण शक्य करण्यासाठी ॲब्स्ट्रॅक्शन तंत्रांवर अवलंबून असतात.

थिअरम प्रूव्हिंग

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

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

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

मॉडेल चेकिंग कॉन्ट्रॅक्ट्सना फायनाईट स्थिती असलेल्या ट्रान्झिशन सिस्टीम्स म्हणून मॉडेल करते, तर थिअरम प्रूव्हिंग अनंत-स्थिती सिस्टीम्सचे विश्लेषण हाताळू शकते. तथापि, याचा अर्थ असा आहे की स्वयंचलित थिअरम प्रूव्हरला नेहमीच हे माहित नसते की लॉजिक समस्या "निर्णय घेण्यायोग्य" (decidable) आहे की नाही.

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

सिम्बॉलिक एक्झिक्यूशन

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

सिम्बॉलिक एक्झिक्यूशन सिम्बॉलिक इनपुट मूल्यांवरील गणितीय सूत्र म्हणून अंमलबजावणी ट्रेसचे प्रतिनिधित्व करते, ज्याला अन्यथा पाथ प्रेडिकेट म्हटले जाते. पाथ प्रेडिकेट "समाधानकारक" (satisfiable) आहे की नाही हे तपासण्यासाठी 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 इथर काढण्याचा प्रयत्न केला तर काय?").

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

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

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

मॅन्युअल श्रमाची किंमत

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

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

फॉल्स निगेटिव्ह्ज

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

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

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

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

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 - इथेरियम स्मार्ट कॉन्ट्रॅक्ट्समधील असुरक्षा शोधण्यासाठी एक सिम्बॉलिक एक्झिक्यूशन टूल