के शोधकर्ता सूचना और स्वचालन में अनुसंधान के लिए राज्य संस्थान (INRIA), Microsoft अनुसंधान और कार्नेगी मेलन विश्वविद्यालय ने प्रस्तुत किया का पहला परीक्षण संस्करण एवर क्रिप्ट क्रिप्टो लाइब्रेरी एवरेस्ट परियोजना के ढांचे के भीतर विकसित किया गया और औपचारिक विश्वसनीयता सत्यापन के गणितीय तरीकों का उपयोग किया गया।
अपनी क्षमताओं और प्रदर्शन के लिए, EverCrypt मौजूदा क्रिप्टो पुस्तकालयों के बहुत करीब है (ओपनएसएसएल) लेकिन उनके विपरीत, विश्वसनीयता और सुरक्षा की अतिरिक्त गारंटी प्रदान करता है।
उदाहरण के सत्यापन प्रक्रिया विस्तृत विनिर्देशों को परिभाषित करने के लिए उबालती है जो कार्यक्रम के सभी व्यवहारों का वर्णन करता है और गणितीय प्रमाण है कि लिखित कोड तैयार विनिर्देशों को पूरा करता है।
साक्ष्य-आधारित गुणवत्ता नियंत्रण विधियों के विपरीत, सत्यापन विश्वसनीय गारंटी प्रदान करता है यह कार्यक्रम केवल डेवलपर्स के रूप में चलेगा और इसमें कोई विशेष प्रकार की त्रुटियां नहीं हैं।
उदाहरण के लिए, विनिर्देश का अनुपालन मेमोरी के साथ सुरक्षित कार्य और त्रुटियों की अनुपस्थिति सुनिश्चित करता है जो बफर अतिप्रवाह की ओर जाता है, डीफ़र्रेंस पॉइंटर्स के लिए, पहले से ही मुक्त किए गए मेमोरी क्षेत्रों तक पहुंचने के लिए, या मेमोरी ब्लॉक्स को डबल करने के लिए।
EverCrypt क्या है?
सदाबहार मजबूत प्रकार और मूल्य जाँच प्रदान करता है- एक घटक कभी भी अन्य गैर-अनुपालन घटक के मापदंडों को पारित नहीं करेगा और अन्य घटकों की आंतरिक स्थिति तक पहुंच प्राप्त नहीं करेगा।
इनपुट / आउटपुट व्यवहार पूरी तरह से सरल गणित फ़ंक्शन क्रियाओं के अनुरूप है, जो क्रिप्टोग्राफिक मानकों में परिभाषित किए गए हैं।
हमलों से बचाने के लिए तीसरे पक्ष के चैनलों में, गणना के दौरान व्यवहार (उदाहरण के लिए, निष्पादन की अवधि या निश्चित मेमोरी तक पहुंच की उपस्थिति) यह उस गुप्त डेटा पर निर्भर नहीं करता है जो संसाधित है।
प्रोजेक्ट कोड कार्यात्मक भाषा में लिखा है F * (एफ स्टार) , जो आश्रित प्रकार और शोधन की एक प्रणाली प्रदान करता है, जो कार्यक्रमों के लिए सटीक विनिर्देशों (गणितीय मॉडल) को स्थापित करने और एसएमटी सूत्रों और सहायक परीक्षण उपकरणों के माध्यम से कार्यान्वयन में त्रुटियों की अनुपस्थिति और त्रुटियों की अनुपस्थिति की गारंटी देने की अनुमति देते हैं।
एफ * में कोड अपाचे 2.0 लाइसेंस के तहत वितरित किया जाता है, और सी में अंतिम मॉड्यूल और एमआईटी लाइसेंस के तहत कोडांतरक।
संदर्भ कोड F * के आधार पर, कोडांतरक, C, OCaml, जावास्क्रिप्ट उत्पन्न होता है और वेब असेंबली कोड।
कोड के कुछ हिस्से तैयार परियोजना में पहले से ही फ़ायरफ़ॉक्स, विंडोज कर्नेल में उपयोग किया जाता है के ब्लॉकचेन Tezos और वीपीएन वायरगार्ड।
सदाबहार घटक
संक्षेप में, EverCrypt HACL * और Vale से दो पहले से अलग परियोजनाओं को जोड़ती हैउनके आधार पर एक एकीकृत एपीआई प्रदान करना और उन्हें वास्तविक परियोजनाओं में उपयोग के लिए उपयुक्त बनाना।
HACL * लो में लिखा है* और इसका लक्ष्य C कार्यक्रमों में उपयोग के लिए क्रिप्टोग्राफिक प्राइमेटिव प्रदान करना है जो वे libsodium और NaCL शैली APIs का उपयोग करते हैं।
अल proyecto Vale ने एक विशिष्ट भाषा विकसित की डोमेन कोडांतरक में सत्यापन बनाने के लिए।
HACL की लगभग 110 हज़ार * कम * भाषा में कोड और Vale के लिए कोड की 25 हज़ार लाइनें संयुक्त हैं और उन्हें सार्वभौमिक भाषा F * में कोड की लगभग 70 हजार पंक्तियों में फिर से लिखा गया है, जिसे भी विकसित किया जा रहा है एवरेस्ट परियोजना के हिस्से के रूप में।
एवर क्रिप्ट लाइब्रेरी का पहला संस्करण सत्यापित कार्यान्वयन की सुविधाएँ निम्नलिखित क्रिप्टोग्राफ़िक एल्गोरिदम के सी या कोडांतरक संस्करणों में प्रस्तावित (उपयोग करते समय)
इनमें से, परियोजना पृष्ठ पर निम्नलिखित स्टैंड आउट हैं:
- हैश एल्गोरिदम: SHA2, SHA3, SHA1 और MD5 के सभी वेरिएंट
- प्रमाणीकरण कोड: डेटा स्रोत प्रमाणीकरण के लिए SHA1, SHA2-256, SHA2-384 और SHA2-512 पर HMAC
- एलएलएफ की जनरेशन एल्गोरिथ्म (HMAC- आधारित विस्तार और निष्कर्षण कुंजी व्युत्पत्ति समारोह)
- ChaCha20 स्ट्रीम एन्क्रिप्शन (गैर-अनुकूलित C संस्करण उपलब्ध)
- Poly1305 संदेश प्रमाणीकरण एल्गोरिथ्म (मैक) (सी और कोडांतरक संस्करण)
- अण्डाकार वक्रों पर डिफी-हेलमैन प्रोटोकॉल Curve25519 (BMI2 और ADX निर्देशों के आधार पर अनुकूलन के साथ C और कोडांतरक संस्करण)
- ब्लॉक एन्क्रिप्शन मोड AEAD (प्रमाणित एन्क्रिप्शन) ChachaPoly (संस्करण C अनुकूलित नहीं)
- AEAD एईएस-जीसीएम ब्लॉक एन्क्रिप्शन मोड (एईएस-एनआई अनुकूलन के साथ कोडांतरक संस्करण)।
पहली बार में अल्फा संस्करण, कोड सत्यापन पहले ही पूरा हो चुका है बड़े पैमाने पर, लेकिन अभी भी कुछ क्षेत्रों को उजागर किया गया है।
इसके अलावा, एपीआई अभी तक स्थिर नहीं है, जिसका विस्तार किया जाएगा निम्नलिखित अल्फा संस्करणों में (यह सभी एपीआई के लिए संरचनाओं को एकजुट करने की योजना है।
दोषों के बीच, x86_64 आर्किटेक्चर के लिए समर्थन को भी हाइलाइट किया गया है (पहले चरण में, मुख्य लक्ष्य विश्वसनीयता है, जबकि अनुकूलन और प्लेटफार्मों को दूसरे स्थान पर लागू किया जाएगा)।
Fuente: https://jonathan.protzenko.fr