औपचारिक रूप से एथेरियम 2.0 चरण 0 विनिर्देशों का सत्यापन

ब्लॉग 1NewsDevelopersEnterpriseBlockchain समझाया और सम्मेलनसमाचार

Contents

हमारे न्यूज़लेटर की सदस्यता लें.

ईमेल पता

हम आपकी निजता का सम्मान करते हैं

HomeBlogBlockchain विकास

औपचारिक रूप से एथेरियम 2.0 चरण 0 विनिर्देशों का सत्यापन

ConsenSys R का एक अपडेट&बीकॉन चेन और एथ 2 की मूल नींव में विश्वसनीयता लाने के उनके प्रयास पर डी। फ्रेंक कास्सेअगुस्ट 10, 2020 द्वारा 10 अगस्त, 2020 को पोस्ट किया गया

dafny ब्लॉग हीरो को सत्यापित करें

ConsenSys R पर स्वचालित सत्यापन टीम&D कुछ महीनों के लिए बीकन चेन के औपचारिक विनिर्देश और सत्यापन पर काम कर रहा है। हमें यह बताते हुए खुशी हो रही है कि बहुत सारी प्रगति हुई है और हालांकि अभी तक पूरी नहीं हुई है, हम विकास करने में सफल रहे हैं बीकन चेन का एक ठोस और औपचारिक रूप से सत्यापित कर्नेल. पहली बार, हमारा काम Eth2.0 इंफ्रास्ट्रक्चर की मूल नींव के लिए भरोसेमंद स्तर का एक बेजोड़ स्तर प्रदान करता है.

क्रियाविधि

सत्यापन बनाम परीक्षण

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

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

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

गुण जो हमने सिद्ध किए हैं 

गुण अनुपस्थिति से लेकर हैं अंकगणित के तहत / overflows तथा दायरे से बाहर सूचकांक, प्रत्येक फ़ंक्शन को तार्किक (प्रथम-क्रम तर्क) पूर्व / पोस्ट-शर्तों के अनुरूप (मर्केलिज़ उदाहरण यहाँ), फ़ंक्शंस की रचनाओं को शामिल करने वाले अधिक जटिल लोगों के लिए। उदाहरण के लिए, हमारे पास निम्नलिखित हैं एसएसजेड की संपत्ति धारावाहिक / वर्णन फ़ंक्शंस: प्रत्येक ऑब्जेक्ट x के लिए, Deserialise (Serialise (x)) = x, अर्थात क्रमबद्ध ऑब्जेक्ट को डीरिसेलाइज़ करने से मूल ऑब्जेक्ट वापस आ जाता है। हमने भी स्थापित किया है आक्रमणकारियों की संख्या, और उन्हें साबित करने के लिए इस्तेमाल किया कि बीकन चेन और फोर्ककॉइन के मुख्य संचालन (State_transition, on_block) वास्तव में ब्लॉकों की एक श्रृंखला का निर्माण: स्टोर में किसी भी ब्लॉक बी के लिए, बी के पूर्वजों ने पूरी तरह से ऑर्डर किए गए अनुक्रम को उत्पत्ति ब्लॉक में ले जाता है, जो ब्लॉकचेन की मुख्य संपत्ति है!

औपचारिक सत्यापन के लाभ

कोई भी औपचारिक पद्धति यह आग्रह करेगी कि सत्यापन एक सुरक्षा सर्वोत्तम अभ्यास है। यहाँ बिल्कुल यही है कि यह पद्धति Ethereum 2.0 के लिए एक सुरक्षित और भरोसेमंद बुनियादी ढाँचा सुनिश्चित करती है.


कार्यात्मक विनिर्देश

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

प्रतिरूपकता

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

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

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

एक ही भाषा में सब कुछ

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

प्रश्न और विचार 

सत्यापन इंजन की ध्वनि के बारे में क्या?

आप सोच रहे होंगे, “क्या होगा अगर डैफी कंपाइलर / वेरिफायर छोटी गाड़ी है?” हम वास्तव में जानते हैं कि डैफी छोटी गाड़ी है (डैफी रेपो मुद्दे), लेकिन हम डैफी में कीड़े की अनुपस्थिति पर भरोसा नहीं करते हैं। हम Dafny (और इसके सत्यापन इंजन) पर भरोसा करते हैं ध्वनि. साउंडनेस का अर्थ है कि जब डैफनी रिपोर्ट करती है कि सबूत सही हैं, तो वे वास्तव में सही हैं. 

क्या होगा यदि हमने जो विनिर्देश लिखा है वह सही नहीं है? 

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

क्या होगा यदि डैफनी यह साबित नहीं कर सकती है कि कार्यान्वयन विनिर्देश के अनुरूप है? 

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

हम आपकी प्रतिक्रिया का स्वागत करते हैं, इसलिए कृपया देखें हमारे eth2.0-dafny रिपॉजिटरी. हम Ethereum 2.0 के विकास को उसके हालिया टेस्टनेट मील के पत्थर तक पहुँचने के लिए उत्साहित कर रहे हैं, और हम नेटवर्क के अगले चरण को सुनिश्चित करने के लिए पारिस्थितिकी तंत्र में टीमों के साथ काम करने के लिए तत्पर हैं।.

आभार: इस पोस्ट के प्रारंभिक संस्करण पर टिप्पणियों के लिए मेरे साथियों जोआन फुलर, रॉबर्टो साल्टिनी (स्वचालित सत्यापन टीम), निकोलस लिओचॉन और एवरी एरविन को धन्यवाद।.

Ethereum 2.0 के साथ रखें

अपने इनबॉक्स में सीधे नवीनतम Eth2 समाचार प्राप्त करने के लिए ConsenSys न्यूज़लेटर की सदस्यता लें. Ethereum 2.0Research और DevelopmentSecurityNewsletter नवीनतम Ethereum समाचार, उद्यम समाधान, डेवलपर संसाधनों और अधिक के लिए हमारे न्यूज़लेटर के लिए सदस्यता लें।कैसे एक सफल ब्लॉकचेन उत्पाद बनाने के लिएवेबिनार

कैसे एक सफल ब्लॉकचेन उत्पाद बनाने के लिए

कैसे सेट अप करें और एक Ethereum नोड चलाएंवेबिनार

कैसे सेट अप करें और एक Ethereum नोड चलाएं

अपनी खुद की Ethereum API कैसे बनायेवेबिनार

अपनी खुद की Ethereum API कैसे बनाये

सोशल टोकन कैसे बनाएंवेबिनार

सोशल टोकन कैसे बनाएं

स्मार्ट अनुबंध विकास में सुरक्षा उपकरणों का उपयोग करनावेबिनार

स्मार्ट अनुबंध विकास में सुरक्षा उपकरणों का उपयोग करना

फ्यूचर ऑफ़ फ़ाइनेंस डिजिटल एसेट्स एंड डेफीवेबिनार

भविष्य का वित्त: डिजिटल एसेट्स और डीआईएफआई

Mike Owergreen Administrator
Sorry! The Author has not filled his profile.
follow me