परिचय
बिटकॉइन और लिक्विड जैसे अन्य ब्लॉकचेन की सुरक्षा, ECDSA और Schnorr हस्ताक्षर जैसे डिजिटल हस्ताक्षर एल्गोरिदम के उपयोग पर निर्भर करती है। एसी लाइब्रेरी को libsecp256k1 कहा जाता है, जिसका नाम अण्डाकार वक्र के नाम पर रखा गया है जिस पर लाइब्रेरी संचालित होती है, इन डिजिटल हस्ताक्षर एल्गोरिदम को प्रदान करने के लिए बिटकॉइन कोर और लिक्विड दोनों द्वारा उपयोग किया जाता है। ये एल्गोरिदम एक गणितीय गणना का उपयोग करते हैं जिसे a कहा जाता है मॉड्यूलर उलटाजो गणना का अपेक्षाकृत महंगा घटक है।
में “तेज़ स्थिर-समय जीसीडी गणना और मॉड्यूलर उलटाडैनियल जे. बर्नस्टीन और बो-यिन यांग ने एक नया मॉड्यूलर व्युत्क्रम एल्गोरिथ्म विकसित किया है। 2021 में, इस एल्गोरिदम को “सेफजीसीडी” कहा गया कार्यान्वित पीटर डेटमैन द्वारा libsecp256k1 के लिए। इस नवीन एल्गोरिदम की जांच प्रक्रिया के हिस्से के रूप में, ब्लॉकस्ट्रीम रिसर्च इसे पूरा करने वाला पहला था औपचारिक सत्यापन औपचारिक रूप से सत्यापित करने के लिए Coq प्रूफ सहायक का उपयोग करके एल्गोरिदम के डिज़ाइन का विश्लेषण करें कि एल्गोरिदम वास्तव में 256-बिट इनपुट पर सही मॉड्यूलर व्युत्क्रम परिणाम के साथ समाप्त होता है।
एल्गोरिथम और कार्यान्वयन के बीच का अंतर
2021 में औपचारिकीकरण के प्रयास ने केवल यह दिखाया कि बर्नस्टीन और यांग द्वारा डिज़ाइन किया गया एल्गोरिदम सही ढंग से काम करता है। हालाँकि, libsecp256k1 में उस एल्गोरिदम का उपयोग करने के लिए C प्रोग्रामिंग भाषा के भीतर सेफजीसीडी एल्गोरिदम के गणितीय विवरण को लागू करने की आवश्यकता होती है। उदाहरण के लिए, एल्गोरिदम का गणितीय विवरण वैक्टर का मैट्रिक्स गुणन करता है जो 256 बिट हस्ताक्षरित पूर्णांक जितना चौड़ा हो सकता है, हालांकि सी प्रोग्रामिंग भाषा मूल रूप से केवल 64 बिट (या कुछ भाषा एक्सटेंशन के साथ 128 बिट) तक पूर्णांक प्रदान करेगी।
सेफजीसीडी एल्गोरिदम को लागू करने के लिए सी के 64 बिट पूर्णांक का उपयोग करके मैट्रिक्स गुणन और अन्य गणनाओं की प्रोग्रामिंग की आवश्यकता होती है। इसके अतिरिक्त, कई अन्य अनुकूलन कार्यान्वयन को तेज़ बनाने के लिए जोड़ा गया है। अंत में, libsecp256k1 में सेफजीसीडी एल्गोरिदम के चार अलग-अलग कार्यान्वयन हैं: हस्ताक्षर पीढ़ी के लिए दो निरंतर समय एल्गोरिदम, एक 32-बिट सिस्टम के लिए अनुकूलित और एक 64-बिट सिस्टम के लिए अनुकूलित, और हस्ताक्षर सत्यापन के लिए दो चर समय एल्गोरिदम, फिर से एक 32-बिट सिस्टम के लिए और एक 64-बिट सिस्टम के लिए।
सत्यापन योग्य सी
यह सत्यापित करने के लिए कि सी कोड सेफजीसीडी एल्गोरिदम को सही ढंग से लागू करता है, सभी कार्यान्वयन विवरणों की जांच की जानी चाहिए। हम उपयोग करते हैं सत्यापन योग्य सीCoq प्रमेय कहावत का उपयोग करके C कोड के बारे में तर्क करने के लिए सत्यापित सॉफ़्टवेयर टूलचेन का हिस्सा।
सत्यापन से गुजरने वाले प्रत्येक फ़ंक्शन के लिए पृथक्करण तर्क का उपयोग करके पूर्व शर्त और उत्तर शर्त निर्दिष्ट करके सत्यापन आगे बढ़ता है। पृथक्करण तर्क सबरूटीन्स, मेमोरी आवंटन, समवर्ती और अधिक के बारे में तर्क करने के लिए एक विशेष तर्क है।
एक बार जब प्रत्येक फ़ंक्शन को एक विनिर्देश दिया जाता है, तो सत्यापन फ़ंक्शन की पूर्व शर्त से शुरू होता है, और फ़ंक्शन के मुख्य भाग में प्रत्येक कथन के बाद एक नया अपरिवर्तनीय स्थापित करता है, जब तक कि अंततः फ़ंक्शन निकाय के अंत में या प्रत्येक के अंत में पोस्ट की स्थिति स्थापित नहीं हो जाती वापसी विवरण. औपचारिकीकरण का अधिकांश प्रयास कोड की पंक्तियों के बीच में खर्च किया जाता है, जिसमें प्रत्येक सी अभिव्यक्ति के कच्चे संचालन को उच्च स्तरीय बयानों में अनुवाद करने के लिए इनवेरिएंट का उपयोग किया जाता है कि हेरफेर की जा रही डेटा संरचनाएं गणितीय रूप से क्या दर्शाती हैं। उदाहरण के लिए, सी भाषा जिसे 64-बिट पूर्णांकों की एक सरणी मानती है, वह वास्तव में 256-बिट पूर्णांक का प्रतिनिधित्व हो सकती है।
अंतिम परिणाम है एक औपचारिक प्रमाणCoq प्रूफ सहायक द्वारा सत्यापित, कि libsecp256k1 का सेफजीसीडी मॉड्यूलर व्युत्क्रम एल्गोरिथ्म का 64-बिट चर समय कार्यान्वयन कार्यात्मक रूप से सही है।
सत्यापन की सीमाएँ
कार्यात्मक शुद्धता प्रमाण की कुछ सीमाएँ हैं। सत्यापन योग्य सी में उपयोग किया जाने वाला पृथक्करण तर्क जिसे कहा जाता है उसे कार्यान्वित करता है आंशिक शुद्धता. इसका मतलब है कि यह केवल C कोड को सही परिणाम के साथ लौटाता है अगर यह वापस आता है, लेकिन यह स्वयं समाप्ति को सिद्ध नहीं करता है। हम इसका उपयोग करके इस सीमा को कम करते हैं हमारा पिछला Coq प्रमाण यह साबित करने के लिए कि मुख्य लूप का लूप काउंटर मान वास्तव में कभी भी 11 पुनरावृत्तियों से अधिक नहीं होता है, यह साबित करने के लिए सेफजीसीडी एल्गोरिदम पर सीमाएं।
एक और मुद्दा यह है कि सी भाषा का कोई औपचारिक विनिर्देश नहीं है। इसके बजाय सत्यापन योग्य C प्रोजेक्ट इसका उपयोग करता है CompCert कंपाइलर प्रोजेक्ट C भाषा का औपचारिक विवरण प्रदान करना। यह गारंटी देता है कि जब एक सत्यापित C प्रोग्राम को CompCert कंपाइलर के साथ संकलित किया जाता है, तो परिणामी असेंबली कोड इसके विनिर्देश (उपरोक्त सीमा के अधीन) को पूरा करेगा। हालाँकि यह गारंटी नहीं देता है कि जीसीसी, क्लैंग, या किसी अन्य कंपाइलर द्वारा उत्पन्न कोड आवश्यक रूप से काम करेगा। उदाहरण के लिए, सी कंपाइलर्स को फ़ंक्शन कॉल के भीतर तर्कों के लिए अलग-अलग मूल्यांकन आदेश देने की अनुमति है। और भले ही सी भाषा में औपचारिक विशिष्टता हो, कोई भी कंपाइलर जो स्वयं औपचारिक रूप से सत्यापित नहीं है, फिर भी प्रोग्राम को गलत तरीके से संकलित कर सकता है। ये करता है घटित होना व्यवहार में।
अंत में, सत्यापन योग्य सी पासिंग संरचनाओं, रिटर्निंग संरचनाओं या असाइनिंग संरचनाओं का समर्थन नहीं करता है। जबकि libsecp256k1 में, संरचनाएं हमेशा पॉइंटर द्वारा पारित की जाती हैं (जिसकी सत्यापन योग्य सी में अनुमति है), ऐसे कुछ अवसर हैं जहां संरचना असाइनमेंट का उपयोग किया जाता है। मॉड्यूलर व्युत्क्रम शुद्धता प्रमाण के लिए, 3 असाइनमेंट थे जिन्हें एक विशेष फ़ंक्शन कॉल द्वारा प्रतिस्थापित किया जाना था जो संरचना असाइनमेंट फ़ील्ड को फ़ील्ड द्वारा निष्पादित करता है।
सारांश
ब्लॉकस्ट्रीम रिसर्च ने औपचारिक रूप से libsecp256k1 के मॉड्यूलर व्युत्क्रम फ़ंक्शन की शुद्धता को सत्यापित किया है। यह कार्य इस बात का और सबूत देता है कि व्यवहार में सी कोड का सत्यापन संभव है। सामान्य प्रयोजन प्रमाण सहायक का उपयोग करने से हमें जटिल गणितीय तर्कों पर निर्मित सॉफ़्टवेयर को सत्यापित करने की अनुमति मिलती है।
libsecp256k1 में कार्यान्वित शेष कार्यों को भी सत्यापित होने से कोई नहीं रोकता है। इस प्रकार libsecp256k1 के लिए उच्चतम संभावित सॉफ़्टवेयर शुद्धता गारंटी प्राप्त करना संभव है।
यह रसेल ओ’कॉनर और एंड्रयू पोलेस्ट्रा की एक अतिथि पोस्ट है। व्यक्त की गई राय पूरी तरह से उनकी अपनी हैं और जरूरी नहीं कि वे बीटीसी इंक या बिटकॉइन मैगज़ीन की राय को प्रतिबिंबित करें।
