एसीएम के संचार में एक वैज्ञानिक लेख प्रकाशित हुआ था, अक्टूबर २०१ p, खंड ६१, संख्या १०, पीपी ६−−::, दोई: १०.११४५ / ३२३०६२ in

फरवरी 2017 में, एक हेलिकॉप्टर ने एरिजोना में बोइंग के हवाई पट्टी से सामान्य मिशन के साथ उड़ान भरी: निकटतम पहाड़ियों के आसपास उड़ान। उन्होंने पूरी तरह से स्वायत्तता से उड़ान भरी। अमेरिकी संघीय उड्डयन प्रशासन की सुरक्षा आवश्यकताओं के अनुसार, पायलट ने नियंत्रणों को नहीं छुआ। यह पहली स्वायत्त उड़ान एएच -6 नहीं थी, जिसे कंपनी अनमैन्ड लिटिल बर्ड (यूएलबी) कहती है। वह कई सालों से इस तरह उड़ रहा है। हालांकि, इस बार उड़ान के बीच में हेलीकॉप्टर ने साइबर हमला किया। ऑन-बोर्ड कंप्यूटर ने कैमकॉर्डर के दुर्भावनापूर्ण सॉफ़्टवेयर पर हमला किया, साथ ही वायरस को संक्रमित फ्लैश ड्राइव के माध्यम से वितरित किया गया, जिसे रखरखाव के दौरान डाला गया था। हमले ने कुछ उप-प्रणालियों को धमकी दी, लेकिन विमान के सुरक्षित संचालन को प्रभावित नहीं कर सका।

मुख्य विचार

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

आप सोच सकते हैं कि सैन्य विमानन आसानी से इस तरह के साइबर हमले को दोहरा सकता है। वास्तव में, 2013 में अत्यधिक विश्वसनीय सैन्य कंप्यूटर सिस्टम हाई-एश्योरेंस साइबर मिलिट्री सिस्टम (HACMS) विकसित करने के लिए DARPA द्वारा कमीशन किए गए पेशेवर पेंटरों की एक टीम ने ULB सॉफ्टवेयर के पहले संस्करण को सफलतापूर्वक हैक किया, जिसे मूल रूप से उड़ान सुरक्षा सुनिश्चित करने के लिए विकसित किया गया था, सुरक्षा नहीं। साइबर हमले से। हैकर्स को हेलीकॉप्टर को क्रैश करने या किसी भी जगह पर लैंड करने का मौका मिलता है। इसलिए, बोर्ड पर एक यात्री के साथ इस तरह के हमलों का जोखिम शायद ही कम किया जा सकता है, और फरवरी 2017 में हैकिंग का एक असफल प्रयास सॉफ्टवेयर में कुछ मूलभूत परिवर्तनों को इंगित करता है।

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

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


मानवरहित परीक्षण उड़ान के दौरान "बर्ड"

सभी हेलिकॉप्टर सॉफ़्टवेयर गणितीय मॉडल और सबूतों पर नहीं बनाए गए हैं। औपचारिक सत्यापन का क्षेत्र अभी इस तरह के पैमाने के लिए तैयार नहीं है। हालांकि, एचएसीएमएस कार्यक्रम ने प्रदर्शित किया है कि समग्र प्रणाली के सबसे महत्वपूर्ण हिस्सों के लिए औपचारिक तरीकों का रणनीतिक अनुप्रयोग सुरक्षा में सुधार करता है। एचएसीएमएस दृष्टिकोण उन प्रणालियों के लिए काम करता है जिनमें वास्तुकला स्तर पर विशुद्ध रूप से प्रवर्तन द्वारा वांछित सुरक्षा सुविधा प्राप्त की जा सकती है। यह हमारे sel4 सत्यापित माइक्रोकर्नेल पर आधारित है, जिसके बारे में हम नीचे बात करेंगे। यह उपतंत्रों के बीच अलगाव की गारंटी देता है, स्पष्ट रूप से परिभाषित संचार चैनलों के अपवाद के साथ जो सिस्टम सुरक्षा नीतियों के अधीन हैं। सिस्टम घटकों के लिए CAmkES सत्यापित ढांचे के साथ वास्तुकला स्तर पर इस अलगाव की गारंटी है। गैलोज़ इंक से डोमेन-विशिष्ट भाषाओं का उपयोग करना CAmkES रॉकवेल कॉलिन्स और मिनेसोटा विश्वविद्यालय से वास्तुकला विश्लेषण उपकरणों के साथ-साथ अत्यधिक विश्वसनीय सॉफ्टवेयर घटकों के साथ एकीकृत करता है।

HACMS की उपलब्धियाँ सॉफ्टवेयर इंजीनियर के पुराने वफादार दोस्त - मॉडर्नाइजेशन पर आधारित हैं। नवाचार यह है कि औपचारिक तरीके इंटरफेस की निगरानी और मॉड्यूल इंटर्नल के इनकैप्सुलेशन को साबित करते हैं। प्रतिरूपकता के लिए यह गारंटीकृत पालन उन इंजीनियरों को अनुमति देता है जो नए तरीकों को बनाने के लिए औपचारिक तरीकों के विशेषज्ञ नहीं हैं (बोइंग में) मौजूदा प्रणालियों को आधुनिक बनाने और उच्च स्थिरता प्राप्त करने के लिए। हालांकि उपकरण अभी तक सिस्टम की सुरक्षा का पूरा सबूत नहीं देते हैं।

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

कार्यक्रमों की गणितीय शुद्धता के साक्ष्य कम से कम 1960 के दशक के हैं , लेकिन लंबे समय तक सॉफ्टवेयर विकास के लिए उनके वास्तविक लाभ गुंजाइश और गहराई में सीमित थे। हालाँकि, हाल के वर्षों में वास्तविक सिस्टम के कोड स्तर पर औपचारिक सत्यापन में कई प्रभावशाली सफलताएँ मिली हैं, सत्यापित C CompCert कंपाइलर से लेकर सत्यापित seL4 माइक्रोकर्नल (इसके बारे में वैज्ञानिक लेख देखें), CoCC सांचा कॉन्फ्रेंसिंग सिस्टम, सत्यापित CakeML ML कंपाइलर, सत्यापित प्रोग्राम मिलवा और कैंडल के प्रमेयों को प्रमाणित करने के लिए, सत्यापित FSCQ विफल- सुरक्षित फाइल सिस्टम, सत्यापित आयरनफ्लेट वितरित प्रणाली और सत्यापित सर्टिकोस समानांतर कर्नेल फ्रेमवर्क , साथ ही महत्वपूर्ण गणितीय प्रमेय, चार रंगों की समस्याओं सहित, केपलर परिकल्पना का स्वचालित प्रमाण और आस्था - थोम्पसन प्रमेय विषम क्रम पर । ये सभी वास्तविक प्रणालियाँ हैं। उदाहरण के लिए, CompCert एक वाणिज्यिक उत्पाद है, seL4 माइक्रोकर्नेल का उपयोग एयरोस्पेस और मानवरहित विमानों में किया जाता है, चीजों के इंटरनेट के मंच के रूप में, और कई बड़े वैज्ञानिक सम्मेलनों में CoCon प्रणाली का उपयोग किया गया है।

इन सत्यापन परियोजनाओं में काफी प्रयास की आवश्यकता होती है। औपचारिक तरीके सार्वजनिक रूप से उपलब्ध कराने के लिए, इन प्रयासों को कम करने की आवश्यकता है। यहां हम प्रदर्शित करते हैं कि कैसे औपचारिक और अनौपचारिक तरीकों का एक रणनीतिक संयोजन, औपचारिक घटकों के आंशिक स्वचालन और अलग-अलग घटकों के लाभों को अधिकतम करने के लिए सावधानीपूर्वक सॉफ्टवेयर विकास ने हमें उन प्रणालियों की विश्वसनीयता में काफी वृद्धि करने की अनुमति दी है जिनके समग्र आकार और जटिलता ऊपर बताए गए लोगों की तुलना में अधिक परिमाण के आदेश हैं।

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

seL4

चलो निर्माण के लिए नींव के साथ शुरू करें विश्वसनीय सिस्टम - ऑपरेटिंग सिस्टम (ओएस) की गिरी। यह सबसे महत्वपूर्ण हिस्सा है जो लागत-प्रभावी तरीके से पूरे सिस्टम की विश्वसनीयता की गारंटी देता है।

SeL4 माइक्रोकर्नेल सुरक्षित सिस्टम को लागू करने के लिए एक औपचारिक रूप से सत्यापित न्यूनतम तंत्र प्रदान करता है। मानक गुठली के विपरीत, यह उद्देश्यपूर्ण सार्वभौमिक है और इसलिए कई सुरक्षा नीतियों और सिस्टम आवश्यकताओं को लागू करने के लिए उपयुक्त है।

SeL4 को विकसित करने के मुख्य लक्ष्यों में से एक है कि कर्नेल के शीर्ष पर चलने वाले पारस्परिक रूप से डिस्ट्रेस्टिंग घटकों के बीच मजबूत अलगाव प्रदान करना। यह पूरी तरह से लिनक्स ऑपरेटिंग सिस्टम के लिए एक हाइपरविजर के रूप में अपने काम का समर्थन करता है, जबकि उन्हें सुरक्षा-महत्वपूर्ण घटकों से अलग रखा जा सकता है जो एक साथ काम कर सकते हैं, जैसा कि चित्र 1 में दिखाया गया है। विशेष रूप से, यह फ़ंक्शन सिस्टम डेवलपर्स को छिपी के साथ विरासत घटकों का उपयोग करने की अनुमति देता है। अत्यधिक विश्वसनीय घटकों के बगल में कमजोरियाँ।


अंजीर। 1. seL4 में अलगाव और नियंत्रित संचार

SeL4 कोर सामान्य माइक्रोन्यूक्लियर के बीच एक विशेष स्थान रखता है। यह न केवल अपनी कक्षा में बेहतर प्रदर्शन प्रदान करता है, सी कोड की इसकी 10,000 लाइनों ने न केवल सबूत लाइनों के संदर्भ में मानव इतिहास में किसी भी अन्य सार्वजनिक रूप से उपलब्ध सॉफ़्टवेयर की तुलना में अधिक कठोर औपचारिक सत्यापन किया है, बल्कि साबित गुणों की ताकत भी है। यह सी में कोर कार्यान्वयन के "कार्यात्मक शुद्धता" के प्रमाण पर आधारित है। यह सुनिश्चित करता है कि कर्नेल के किसी भी व्यवहार की भविष्यवाणी उसके औपचारिक सार विनिर्देश द्वारा की जाती है: यह सबूत कैसे दिखता है, इस विचार के लिए ऑनलाइन आवेदन देखें। इस गारंटी के बाद, हमने अतिरिक्त सबूत जोड़े हैं जो हम नाभिक के बुनियादी तंत्र से परिचय के बाद बताएंगे।

seL4 एपीआई

SeL4 कर्नेल सुरक्षित प्रणालियों को लागू करने के लिए न्यूनतम तंत्र प्रदान करता है: धाराएँ, क्षमता प्रबंधन, आभासी पता स्थान, इंटरप्रोसेस संचार (IPC), सिग्नलिंग और इंटरप्ट डिलीवरी।

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

थ्रेड इंटरप्रोसेस संचार "एंडपॉइंट्स" के माध्यम से संदेश भेजकर बातचीत और सिंक्रनाइज़ करते हैं। संबंधित समापन बिंदु पर भेजने की क्षमता वाला एक धागा दूसरे छोर पर एक संदेश भेज सकता है जिसमें इस समापन बिंदु को प्राप्त करने की क्षमता है। अधिसूचना ऑब्जेक्ट बाइनरी सेमाफोर के सेट में सिंक्रनाइज़ेशन प्रदान करते हैं। वर्चुअल एड्रेस ट्रांसलेशन को कर्नेल ऑब्जेक्ट्स द्वारा नियंत्रित किया जाता है जो संबंधित प्रोसेसर आर्किटेक्चर ऑब्जेक्ट्स पर पेज डाइरेक्टरीज़, पेज टेबल और फ्रेम ऑब्जेक्ट्स या सूक्ष्म अमूर्त का प्रतिनिधित्व करते हैं। प्रत्येक स्ट्रीम में एक निश्चित "वेस्पेस" क्षमता होती है, जो स्ट्रीम एड्रेस ट्रांसलेशन ऑब्जेक्ट्स के पेड़ की जड़ की ओर इशारा करती है। क्षमताओं को स्वयं कर्नेल द्वारा प्रबंधित किया जाता है और ग्राफ़ की संरचना में स्थित "CNodes" कर्नेल ऑब्जेक्ट में संग्रहीत होता है, जो एक्सेस अधिकारों के साथ ऑब्जेक्ट्स से लिंक करता है, मेमोरी में भौतिक पतों के साथ वर्चुअल पेज तालिकाओं की तुलना करने के समान है। जड़ CNode की पहचान करने के लिए प्रत्येक थ्रेड की अपनी क्षमता है। इस रूट से उपलब्ध क्षमताओं का सेट, जिसे हम "CSpace Stream" कहते हैं। उपयोगिताओं को नौकरी हस्तांतरण के साथ समापन बिंदुओं के माध्यम से स्थानांतरित किया जा सकता है, और उन्हें आम सीएसपी का उपयोग करके साझा भी घोषित किया जा सकता है। चित्र 2 इन कर्नेल ऑब्जेक्ट्स को दिखाता है।


अंजीर। 2. एक seL4 प्रणाली में कर्नेल ऑब्जेक्ट दो थ्रेड्स के साथ एक समापन बिंदु के माध्यम से बातचीत करते हैं

सुरक्षा साक्ष्य

इसकी बहुमुखी प्रतिभा के कारण, seL4 कर्नेल API निम्न-स्तरीय हैं और अत्यधिक गतिशील सिस्टम आर्किटेक्चर का समर्थन करते हैं। इसलिए, इन एपीआई के लिए प्रत्यक्ष प्रमाण प्राप्त करना मुश्किल है।

व्यक्तिगत वस्तुओं और कर्नेल क्षमताओं से अभिगम नियंत्रण नीतियों के सार की उच्च-स्तरीय अवधारणा, अमूर्त "विषयों" (घटकों) के एक समूह का उपयोग करके सिस्टम के अभिगम नियंत्रण विन्यास को कैप्चर करना और उनमें से प्रत्येक के पास जो शक्तियां हैं (उदाहरण के लिए, डेटा पढ़ने और संदेश भेजने के लिए) । अंजीर में उदाहरण में। 2, घटक ए और बी ने समापन बिंदु पर अधिकार प्राप्त किया।

सीवेल और सहकर्मियों ने साबित किया है कि seL4 एक्सेस कंट्रोल पॉलिसी यह सुनिश्चित करती है कि दो बुनियादी सुरक्षा सुविधाओं का सम्मान किया जाए: विशेषाधिकार प्रतिबंध और अखंडता।

प्राधिकरण के प्रतिबंध का मतलब है कि एक्सेस कंट्रोल पॉलिसी किसी भी भविष्य की स्थिति के लिए सिस्टम में विशिष्ट क्षमताओं और कर्नेल ऑब्जेक्ट्स का एक स्थिर (अपरिवर्तित) सुरक्षित सन्निकटन है। यह गुण बताता है कि सिस्टम कैसे विकसित होता है, कोई भी घटक एक्सेस कंट्रोल पॉलिसी की तुलना में कभी भी अधिक अधिकार प्राप्त नहीं करेगा। चित्रा 2 में, घटक बी के लिए नीति में घटक ए तक पहुंच नहीं है। इस प्रकार, घटक बी भविष्य में कभी भी इस पहुंच को प्राप्त करने में सक्षम नहीं होगा। इस संपत्ति का अर्थ है कि नीति के स्तर पर तर्क प्रणाली में अभिगम नियंत्रण की विशिष्ट स्थिति के बारे में तर्क करने के लिए एक सुरक्षित सन्निकटन है।

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

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

SeL4 में आगे के प्रमाण में कार्यात्मक शुद्धता का विस्तार शामिल है और इसलिए, ARMv7 वास्तुकला के लिए एक द्विआधारी स्तर पर सुरक्षा प्रमेय और कर्नेल ( 1 , 2 ) के लिए सबसे खराब स्थिति रनटाइम प्रोफ़ाइल है, जो वास्तविक समय प्रणालियों के लिए आवश्यक है। SeL4 कोर विभिन्न आर्किटेक्चर के लिए उपलब्ध है: ARMv6, ARMv7 ARMv7a, ARMv8, RISC-V, Intel x86 और Intel x64। फिलहाल, इसने पूरे सत्यापन स्टैक के लिए ARMv7 आर्किटेक्चर पर मशीन परीक्षण पास किया है, साथ ही कार्यात्मक शुद्धता के लिए हाइपरविजर एक्सटेंशन के साथ ARMv7a पर।

वास्तुकला सुरक्षा

पिछले अनुभाग ने उन प्रोग्रामिंग विधियों का वर्णन किया है जिनके द्वारा seL4 कर्नेल काफी विश्वसनीय प्रणालियों के लिए एक ठोस आधार बनाता है। कर्नेल एक विश्वसनीय कंप्यूटिंग बेस (टीसीबी) बनाता है - सॉफ्टवेयर का एक अनिवार्य घटक जो सिस्टम सुरक्षा की गारंटी के लिए सही ढंग से काम करना चाहिए। वास्तविक प्रणालियों में, यह आधार सिर्फ एक माइक्रोकर्नेल की तुलना में बहुत व्यापक है। कर्नेल के लिए आत्मविश्वास के समान स्तर प्राप्त करने के लिए एक अतिरिक्त सॉफ्टवेयर स्टैक को सत्यापित करना आवश्यक है। हालांकि, ऐसी प्रणालियों की कक्षाएं हैं जिनके लिए इस तरह के सत्यापन की कोई आवश्यकता नहीं है: सिस्टम स्तर पर कुछ सुरक्षा गुणों को प्राप्त करने के लिए उन्हें कर्नेल स्तर पर अलगाव प्रमेयों की आवश्यकता होती है। यह खंड ऐसी प्रणाली का एक उदाहरण प्रदान करता है।

ये ऐसी प्रणालियां हैं जिनमें घटक आर्किटेक्चर पहले से ही एक महत्वपूर्ण संपत्ति को लागू कर चुके हैं, शायद कई छोटे विश्वसनीय घटकों के साथ। हमारा उदाहरण क्वाडकॉप्टर फ्लाइट कंट्रोल सॉफ्टवेयर है, जो पहले उल्लेखित एचएसीएमएस कार्यक्रम में एक डेमो डिवाइस है।

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


अंजीर। 3. एक स्वायत्त विमान की वास्तुकला

यह आंकड़ा दो मुख्य कंप्यूटरों को दिखाता है: एक ऑन-बोर्ड कंप्यूटर जो ग्राउंड स्टेशन के साथ संचार करता है और बोर्ड पर सॉफ़्टवेयर को नियंत्रित करता है (उदाहरण के लिए, कैमरा), और वाहन की उड़ान को नियंत्रित करने के लिए एक नेविगेशन कंप्यूटर, सेंसर डेटा, और नियंत्रण इंजन पढ़ें। कंप्यूटर एक आंतरिक नेटवर्क के माध्यम से जुड़े हुए हैं या एक ट्रैक्टर पर कर सकते हैं, ULB पर ईथरनेट। क्वाड्रोकॉप्टर में एक असुरक्षित वाईफाई बिंदु भी है, जो अतिरिक्त सुरक्षा विधियों को प्रदर्शित करना संभव बनाता है।

इस उदाहरण में, एक ऑन-बोर्ड कंप्यूटर पर विचार करें। चार बुनियादी गुणों को पूरा किया जाना चाहिए:

• ग्राउंड स्टेशन से आदेशों का उचित प्रमाणीकरण;
  
• क्रिप्टोग्राफिक कुंजी की गोपनीयता;
  
• नेविगेशन कंप्यूटर के लिए कोई अतिरिक्त संदेश नहीं;
  
• अन्य ऑन-बोर्ड सिस्टम से अविश्वसनीय सॉफ्टवेयर डिवाइस की उड़ान को प्रभावित नहीं कर सकता है।

काम की परिकल्पना यह है कि कैमरा अविश्वसनीय, संभावित रूप से समझौता या दुर्भावनापूर्ण है, कि इसके ड्राइवर और पुराने सॉफ़्टवेयर संभावित रूप से समझौता किए जाते हैं, साथ ही साथ कोई बाहरी संचार चैनल भी। इस उदाहरण में, हम सही और मजबूत क्रिप्टोग्राफी मानते हैं, यानी कि कुंजी को उठाया नहीं जा सकता है, और हम दुश्मन के रेडियो संचार को एक ग्राउंड स्टेशन के साथ दबाने के लिए कार्य के दायरे से परे जाते हैं।

चित्र 4 दिखाता है कि इन गुणों को प्रदान करने के लिए क्वाड्रोकॉप्टर वास्तुकला कैसे डिज़ाइन की गई है। लिनक्स वर्चुअल मशीन (VM) विरासत में ऑन-बोर्ड डिवाइस सॉफ्टवेयर, कैमरा ड्राइवर और वाईफाई हॉटस्पॉट के लिए एक कंटेनर के रूप में कार्य करता है। हम अपने स्वयं के घटक में क्रिप्टोग्राफी नियंत्रण मॉड्यूल को कैन स्टेशन, जमीन स्टेशन चैनल और लिनक्स वर्चुअल मशीन के साथ जमीन स्टेशन पर डेटा भेजने के लिए अलग करते हैं। क्रिप्टोग्राफ़िक घटक का कार्य ऑन-बोर्ड कंप्यूटर पर स्टैक के CAN इंटरफ़ेस के माध्यम से (केवल) अधिकृत संदेशों को प्रसारित करना और नैदानिक ​​डेटा को वापस ग्राउंड स्टेशन पर भेजना है। रेडियो घटक क्रिप्टोग्राफिक घटक द्वारा एन्क्रिप्ट किए गए और डिक्रिप्ट किए गए (प्रमाणीकरण के साथ) कच्चे संदेश भेजता है और प्राप्त करता है।


चित्र 4। सरलीकृत क्वाडकॉप्टर ऑन-बोर्ड कंप्यूटर आर्किटेक्चर

सिस्टम के वांछित गुणों को सेट करना विशेष रूप से अलगाव के गुणों और सूचना प्रवाह के संदर्भ में वास्तुकला के व्यवहार के साथ-साथ एकल विश्वसनीय क्रिप्टोग्राफिक घटक के व्यवहार के लिए कम हो जाता है। इस घटक के सही व्यवहार को मानते हुए, कुंजियों से समझौता नहीं किया जा सकता है, क्योंकि किसी अन्य घटक की उन तक पहुंच नहीं है। अंजीर में लिनक्स और क्रिप्टोग्राफिक घटक के बीच का चैनल। 4 केवल मैसेजिंग के लिए है और यह मेमोरी को एक्सेस नहीं देता है। केवल अधिकृत संदेश ही CAN बस में जा सकते हैं, क्योंकि क्रिप्टोग्राफिक घटक बस के साथ एकमात्र संचार है। लिनक्स वर्चुअल मशीन के हिस्से के रूप में अविश्वसनीय सॉफ्टवेयर और वाईफाई, घटक अलगाव द्वारा समझाया जाता है और केवल विश्वसनीय क्रिप्टोग्राफिक घटक के माध्यम से बाकी सिस्टम के साथ बातचीत कर सकता है।

यह कल्पना करना आसान है कि उच्च स्तर के यांत्रिक तर्क के मॉडल और उपकरणों की जांच करके वास्तुकला के इस तरह के विश्लेषण को काफी हद तक स्वचालित किया जा सकता है। जैसा कि MILS सिस्टम के लिए जाना जाता है , इस तरह के आर्किटेक्चर में घटकों की सीमाएं न केवल विभाजन और कोड प्रबंधन के लिए एक सुविधाजनक उपकरण हैं, लेकिन मजबूर अलगाव के साथ प्रणाली के व्यवहार के बारे में औपचारिक तर्क के लिए प्रभावी सीमाएं प्रदान करती हैं। हालांकि, यह सभी अंतिम बाइनरी सिस्टम कार्यान्वयन में रन समय पर घटक सीमाओं के उचित अनुप्रयोग पर निर्भर करता है।

SeL4 कर्नेल की पहले से चर्चा की गई तंत्र इस तरह के कार्यान्वयन को प्रदान करने में सक्षम हैं, लेकिन आर्किटेक्चरल स्कीम के ब्लॉक और एरो के साथ तंत्र के अमूर्त के स्तर में तेजी से विरोधाभास है: एक और भी अमूर्त अभिगम नियंत्रण नीति में अभी भी आर्किटेक्चर स्कीम की तुलना में बहुत अधिक विवरण हैं। इस आकार की एक वास्तविक प्रणाली में, हज़ारों कर्नेल ऑब्जेक्ट और "क्षमताएं" सॉफ़्टवेयर द्वारा बनाई गई हैं, और कॉन्फ़िगरेशन त्रुटियों से सुरक्षा उल्लंघन हो सकते हैं। फिर हम चर्चा करते हैं कि कैसे हम न केवल इस तरह के कोड के विन्यास और निर्माण को स्वचालित करते हैं, बल्कि यह भी कि वास्तुकला की सीमाओं के साथ अनुपालन को स्वचालित रूप से कैसे साबित किया जाए।

घटक देखें सत्यापन

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


अंजीर। 5. CAmkES वर्कफ़्लो

कोड जनरेशन

आंतरिक रूप से, CAmkES seL4 में निम्न-स्तरीय कर्नेल ऑब्जेक्ट का उपयोग करके इन सार को लागू करता है। प्रत्येक घटक में (कम से कम) एक स्ट्रीम, CSpace और VSpace शामिल हैं। RPC कनेक्टर एंडपॉइंट ऑब्जेक्ट का उपयोग करते हैं, और CAmkES संदेशों को संसाधित करने और उन्हें IPC समापन बिंदु पर भेजने के लिए मध्यवर्ती कोड उत्पन्न करता है। इसी प्रकार, डेटापोर्ट कनेक्टर को साझा मेमोरी के माध्यम से कार्यान्वित किया जाता है - दो घटकों के पता स्थानों में मौजूद सामान्य फ़्रेम - और वैकल्पिक रूप से डेटा ट्रांसफर की दिशा को सीमित कर सकते हैं। अंत में, घटना कनेक्टर को seL4 अधिसूचना तंत्र का उपयोग करके लागू किया गया है।

CAmkES भी capDL में वस्तुओं के प्रारंभिक विन्यास और सिस्टम के कर्नेल की क्षमताओं के निम्न-स्तरीय विनिर्देश उत्पन्न करता है। यह विनिर्देश seL4 इनिशियलाइज़र के लिए इनपुट बन जाता है, जोयह लोड करने के बाद पहले शुरू होता है और एक उदाहरण बनाने और सिस्टम को इनिशियलाइज़ करने के लिए आवश्यक seL4 ऑपरेशन करता है ।

इस प्रकार, घटक प्लेटफ़ॉर्म डेवलपर की ओर से अतिरिक्त प्रयास के बिना कोड उत्पन्न करता है। घटक वास्तुकला ब्लॉक और तीर का एक सेट का वर्णन करता है, और कार्यान्वयन कार्य केवल खेतों में भरने के लिए नीचे आता है। मंच बाकी को उत्पन्न करता है, वर्णित वास्तुकला का कार्यान्वयन प्रदान करता है।

पारंपरिक घटकों के साथ एक मंच पर, उत्पन्न कोड सिस्टम के विश्वसनीय कंप्यूटिंग बेस का विस्तार करेगा, क्योंकि यह घटकों की कार्यक्षमता को प्रभावित कर सकता है। हालांकि, CAmkES भी सबूत पैदा करता है।

ऑटो सबूत

"इंटरमीडिएट" कोड बनाते समय, CAmkES इसाबेल / HOL में औपचारिक प्रमाण प्रस्तुत करता है, अनुवाद के दौरान सत्यापन करता है और यह प्रदर्शित करता है कि उत्पन्न "मध्यवर्ती" कोड उच्च-स्तरीय विनिर्देश का पालन करता है, और उत्पन्न capDL विनिर्देश CAmkES विवरण का सही विनिर्देश है । हमने यह भी साबित किया है कि seL4 इनिशियलाइज़र सिस्टम को आवश्यक प्रारंभिक कॉन्फ़िगरेशन में सही ढंग से कॉन्फ़िगर करता है। उसी समय, हम भरोसेमंद कंप्यूटिंग बेस का विस्तार किए बिना सिस्टम के अधिकांश निर्माण को स्वचालित करते हैं।

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


अंजीर। 6. जनरेट किया गया RPC कोड

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

आज तक, हमने इस प्रक्रिया को विशेष CAmkES RPC कनेक्टर ( 1 , 2 ) का उपयोग करके शुरू से अंत तक प्रदर्शित किया है । चूंकि अन्य कनेक्टर (डेटापार्ट और इवेंट) के लिए टेम्पलेट आरपीसी की तुलना में बहुत सरल हैं, इसलिए इन कनेक्टर का समर्थन करने के लिए साक्ष्य जनरेटर का विस्तार करना मुश्किल नहीं होगा, जो आपको अधिक विविध सत्यापित सिस्टम बनाने की अनुमति देगा।

संचार कोड के बाद, वास्तुकला की सीमाओं को लागू करने के लिए CAmkES प्रारंभिक अभिगम नियंत्रण विन्यास बनाता है। यह साबित करने के लिए कि ये दो सिस्टम विवरण - कैपडल और CAmkES - एक दूसरे से मेल खाते हैं, CAmkES विवरण को capDL विवरण के लिए अमूर्त के रूप में मानते हैं। हम पहले परीक्षण किए गए ढांचे का उपयोग कैप्डल विवरण से किसी अन्य वस्तु पर एक वस्तु के अधिकार को प्राप्त करने के लिए करते हैं। इसलिए हम सबूतों को राजनीति के स्तर तक बढ़ाएंगे। इसके अलावा, हमने CAmkES विवरण में घटकों के बीच अधिकार वापस लेने के नियमों को परिभाषित किया। यह प्रमाण सुनिश्चित करता है कि कैप्डल वस्तुओं को एक विशेषाधिकार ग्राफ के रूप में दर्शाया जाता है, जिसमें घटकों द्वारा वर्गीकृत वस्तुओं को समूहों के बीच समान सीमा होती है, जैसा कि बराबर सीएएमकेईएस घटक ग्राफ में होता है।। सहज रूप से, सीमाओं के इस पत्राचार का मतलब है कि सीएएमकेईएस विवरण से पॉलिसी आर्किटेक्चर का विश्लेषण कैप्डल द्वारा उत्पन्न विवरण से नीति को बचाएगा, जो बदले में, प्राधिकरण प्रतिबंध, अखंडता और गोपनीयता की आवश्यकताओं को पूरा करने की गारंटी है, जैसा कि पहले उल्लेख किया गया है।

अंत में, सही आरंभीकरण को साबित करने के लिए, CAmkES एक सार्वभौमिक इनिशियलाइज़र का उपयोग करता है जो लोड करने के बाद पहले उपयोगकर्ता कार्य के रूप में शुरू होता है। SeL4 में, यह पहला (और अनोखा) उपयोगकर्ता कार्य सभी उपलब्ध मेमोरी तक पहुंच रखता है, इसका उपयोग ऑब्जेक्ट्स और "क्षमताओं" को capDL के विस्तृत विवरण के अनुसार करने के लिए करता है, जिसे वह इनपुट के रूप में स्वीकार करता है। यह सिद्ध है किइनिशियलाइज़र के निष्पादन के बाद राज्य निर्दिष्ट विनिर्देश में वर्णित राज्य को संतुष्ट करता है । यह प्रमाण सटीक आरंभिक मॉडल के लिए सही है, लेकिन कार्यान्वयन स्तर पर अभी तक नहीं है। बाकी साक्ष्य श्रृंखला की गहराई की तुलना में, यह सीमा कमजोर लग सकती है, लेकिन सामान्य सुरक्षा मूल्यांकन मानदंडों के उच्चतम स्तर (ईएएल 7) पर पहले से अधिक औपचारिक साक्ष्य होना आवश्यक है।

भूकंपीय सुरक्षा उन्नयन

व्यवहार में, सुरक्षा के लिए खरोंच से एक प्रणाली के विकास को सुनिश्चित करना मुश्किल है, इसलिए पुराने सॉफ़्टवेयर को अपग्रेड करने की क्षमता सुरक्षित प्रणालियों के विकास के लिए महत्वपूर्ण है। हमारा seL4- आधारित ढांचा एक पुनरावृत्त प्रक्रिया का समर्थन करता है जिसे हम "भूकंपीय सुरक्षा उन्नयन" कहते हैं, क्योंकि एक नियमित वास्तुकार अधिक भूकंपीय स्थिरता के लिए मौजूदा भवनों का उन्नयन करेगा। हम एक मानवरहित हेलीकॉप्टर के मौजूदा सॉफ्टवेयर आर्किटेक्चर के क्रमिक अनुकूलन के उदाहरण द्वारा प्रक्रिया का वर्णन करते हैं, जो पारंपरिक परीक्षण योजना से औपचारिक तरीकों द्वारा समर्थित प्रमेयों के साथ अत्यधिक विश्वसनीय प्रणाली की ओर बढ़ रहा है। हालाँकि यह उदाहरण एक वास्तविक ULB परियोजना पर आधारित है, यह यहाँ सरल है और इसमें सभी विवरण शामिल नहीं हैं।

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

चरण 1. वर्चुअलाइजेशन

पहला कदम सिस्टम को लेना था जैसा कि यह है और इसे एक वर्चुअल मशीन में एक सुरक्षित हाइपरवाइजर के ऊपर चलाएं (चित्र 7 देखें)। भूकंपीय आधुनिकीकरण के रूपक में, यह सिस्टम को अधिक मोबाइल नींव पर रखने से मेल खाता है। इस प्रणाली में seL4 के शीर्ष पर एक वर्चुअल मशीन में एक CAmkES घटक होता है, जिसमें एक वर्चुअल मशीन मॉनीटर (VMM) और एक अतिथि ऑपरेटिंग सिस्टम शामिल होता है, इस मामले में Linux। कर्नेल वर्चुअलाइजेशन हार्डवेयर एब्स्ट्रैक्ट प्रदान करता है, और VMM वर्चुअल मशीन के लिए इन एब्स्ट्रैक्ट को मैनेज करता है। SeL4 कर्नेल न केवल अतिथि OS, बल्कि VMM को भी सीमित करता है, इसलिए आपको मजबूर अलगाव प्रदान करने के लिए VMM कार्यान्वयन पर भरोसा करने की आवश्यकता नहीं है। VMM विफलता के परिणामस्वरूप अतिथि OS की विफलता होगी, लेकिन संपूर्ण सिस्टम की विफलता नहीं।


अंजीर। 7. एक आभासी मशीन में सभी कार्यक्षमता

सिस्टम कॉन्फ़िगरेशन के आधार पर, वर्चुअल मशीन में पैरावर्चुअलाइज्ड ड्राइवरों, पास-थ्रू ड्राइवरों या दोनों के माध्यम से उपकरणों तक पहुंच हो सकती है। पास-थ्रू ड्राइवरों के मामले में, डेवलपर्स अतिथि सिस्टम में हार्डवेयर उपकरणों और ड्राइवरों द्वारा अलगाव सीमाओं के उल्लंघन को रोकने के लिए सिस्टम MMU या IOMMU का उपयोग कर सकते हैं। कृपया ध्यान दें कि केवल वर्चुअल मशीन में सिस्टम शुरू करने से अतिरिक्त सुरक्षा या विश्वसनीयता लाभ नहीं जुड़ते हैं। चरण 2 की तैयारी के लिए केवल चरण 1 की आवश्यकता है।

चरण 2. कई आभासी मशीनें

भूकंपीय आधुनिकीकरण का दूसरा चरण मौजूदा दीवारों को मजबूत करता है। सॉफ्टवेयर में, एक डेवलपर स्रोत प्रणाली को कई उप-प्रणालियों में विभाजित करके सुरक्षा और विश्वसनीयता बढ़ा सकता है, जिनमें से प्रत्येक में एक वर्चुअल मशीन होती है जो केवल स्रोत प्रणाली कोड का हिस्सा चलती है। प्रत्येक वीएम / वीएमएम संयोजन एक अलग सीएएमकेईएस घटक में किया जाता है, जो विभिन्न उप-प्रणालियों के बीच अलगाव का परिचय देता है, उन्हें एक दूसरे को प्रभावित करने की अनुमति नहीं देता है, और फिर सुरक्षा के विभिन्न स्तरों के सह-अस्तित्व की अनुमति देता है।

सामान्य तौर पर, अनुभाग मौजूदा सॉफ़्टवेयर आर्किटेक्चर का अनुसरण करते हैं, हालांकि यदि प्रभावी अलगाव के लिए वास्तुकला पर्याप्त नहीं है, तो रीडिज़ाइन की आवश्यकता हो सकती है।

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

स्रोत प्रणाली के सबसिस्टम का प्रतिनिधित्व करने वाली आभासी मशीनों के अलावा, हम किसी भी साझा संसाधनों (जैसे नेटवर्क इंटरफ़ेस) के लिए घटकों को भी निकालते हैं और लागू करते हैं।

आप चरण 2 को तब तक दोहरा सकते हैं जब तक कि हम वर्गों के वांछित विवरण तक नहीं पहुँच जाते। सही डिटेलिंग एक तरफ इन्सुलेशन ताकत के बीच एक समझौता है, और दूसरी ओर संचार संचार और पुनर्निर्माण लागत में वृद्धि हुई है।

हमारे उदाहरण में, हमें तीन खंड मिले: एक वर्चुअल मशीन जो लिनक्स चलाने वाले ग्राउंड स्टेशन के संचार कार्यों को लागू करती है; एक और आभासी मशीन जो कैमरा-आधारित नेविगेशन फ़ंक्शंस (भी लिनक्स चला रही है) को लागू करती है; और एक देशी नेटवर्क साझा करने वाला घटक, जैसा कि अंजीर में दिखाया गया है। 8।


चित्र 8। कार्यक्षमता कई आभासी मशीनों में विभाजित है

चरण 3. मूल घटक

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

मूल घटक एक घटक की विश्वसनीयता बढ़ाने के लिए औपचारिक सत्यापन और अन्य तरीकों को लागू करने की क्षमता भी बढ़ाते हैं। विकल्प अलग-अलग हैं: देशी कोड के पूर्ण कार्यात्मक सत्यापन से लेकर संयुक्त पीढ़ी के कोड और साक्ष्य, मॉडल सत्यापन, टाइप-सुरक्षित प्रोग्रामिंग भाषाओं का उपयोग, स्थैतिक विश्लेषण या छोटे कोड आधार के पारंपरिक कठोर परीक्षण।

SeL4 और घटक वास्तुकला द्वारा प्रदान किए गए अलगाव के लिए धन्यवाद, विश्वसनीयता के विभिन्न स्तरों के साथ घटकों की एक प्रणाली में एक साथ काम करना संभव है। इस मामले में, कम विश्वसनीयता वाले घटक सिस्टम की समग्र विश्वसनीयता को कम नहीं करते हैं, और डेवलपर्स इस तथ्य से लाभान्वित होते हैं कि आपको इस कोड को सत्यापित करने पर प्रयास करने की आवश्यकता नहीं है।

हमारे उदाहरण में, हम ऑन-बोर्ड कंप्यूटर और ग्राउंड स्टेशन के बीच देशी मॉड्यूल में संचार चैनल के लिए वर्चुअल मशीन का विश्लेषण करेंगे। देशी घटकों में संचार, क्रिप्टोग्राफी और नियंत्रण कार्य (मिशन-प्रबंधक) कार्यान्वित किए जाते हैं। हम वर्चुअल मशीन में कैमरा और वाईफाई को एक अविश्वसनीय अप्रचलित घटक के रूप में छोड़ देंगे (चित्र 9 देखें)। यह पृथक्करण उप-प्रणालियों के रीमेक और प्रदर्शन और विश्वसनीयता के मामले में देशी घटकों के उपयोग के लाभों के बीच एक समझौता बन गया है।


अंजीर। 9. देशी घटकों में क्रियाशीलता

चरण 4. एक पूरे के रूप में सिस्टम की विश्वसनीयता

सभी आवश्यक मॉड्यूल प्राप्त करने के बाद, हम अंतिम चरण लेंगे: वास्तुकला और व्यक्तिगत घटकों की विश्वसनीयता के आधार पर संपूर्ण प्रणाली का विश्लेषण।

HACMS के ढांचे के भीतर, संचार, क्रिप्टोग्राफी, और एक नियंत्रण मॉड्यूल को ढेर पर स्मृति की एक निश्चित मात्रा के आवंटन के साथ, काफी प्रकार-सुरक्षित ऑब्जेक्ट-ओरिएंटेड भाषा आइवरी में लागू किया जाता है। अतिरिक्त सत्यापन के बिना, आइवरी हमें कार्यात्मक शुद्धता की गारंटी नहीं देता है, लेकिन दोष सहिष्णुता और आपातकालीन विश्वसनीयता में विश्वास दिलाता है। घटकों के अलगाव को देखते हुए, हम मानते हैं कि ये वारंटी अविश्वसनीय घटकों (जैसे कैमरा वर्चुअल मशीन) की उपस्थिति में रहते हैं।

नेटवर्क घटक मानक सी कोड पर लागू किया जाता है, जिसमें प्लेटफ़ॉर्म और मौजूदा लाइब्रेरी कोड के लिए उपयोगकर्ता कोड होते हैं। इसकी विश्वसनीयता का स्तर अच्छी तरह से ज्ञात कोड के सावधानीपूर्वक कार्यान्वयन के माध्यम से प्राप्त स्तर से मेल खाता है। ड्राइवर संश्लेषण जैसे तरीकों के साथ-साथ आइवरी जैसी सुरक्षित-सुरक्षित भाषाओं का उपयोग करके बहुत अधिक खर्च के बिना विश्वसनीयता में सुधार किया जा सकता है। सिस्टम सुरक्षा के एक सामान्य विश्लेषण में, नेटवर्क घटक का कोई भी समझौता केवल नेटवर्क पैकेट को प्रभावित करेगा। चूंकि ट्रैफ़िक एन्क्रिप्ट किया गया है, इस तरह के हमले से उन विशिष्टताओं की स्थिति को खतरा नहीं होगा जो केवल अधिकृत कमांड ऑन-बोर्ड कंप्यूटर में मिलते हैं।

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

सीमाएं और भविष्य का काम

यह आलेख सिस्टम के लिए बहुत उच्च स्तर की सुरक्षा प्राप्त करने के लिए विधि का अवलोकन प्रदान करता है जिसमें घटक वास्तुकला के माध्यम से सुरक्षा सुविधा लागू होती है। हमने कर्नेल स्तर और इसके सही कॉन्फ़िगरेशन के लिए प्रमेय सिद्ध किए हैं, साथ ही प्रमेय भी गारंटी देते हैं कि घटक प्लेटफ़ॉर्म इसकी वास्तुकला के विवरण के अनुसार सुरक्षा सीमाओं को सही ढंग से निर्धारित करता है, और यह दूरस्थ प्रक्रिया कॉल के लिए सही कोड उत्पन्न करता है। सिस्टम के उच्च-स्तरीय सुरक्षा विश्लेषण के साथ संबंध अनौपचारिक बना हुआ है, और संचार कोड प्रमेय प्लेटफॉर्म द्वारा प्रदान किए गए सभी संचार प्राइमेट को कवर नहीं करते हैं। स्वचालित रूप से एक प्रमेय प्राप्त करने के लिए जो पूरे सिस्टम को शुरू से अंत तक कवर करता है, अतिरिक्त काम की आवश्यकता होती है। हालाँकि, इस स्तर पर यह स्पष्ट है कि यह एक संभव कार्य है।

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

इन सीमाओं को आसान बनाने के लिए पहला कदम ऐसे आर्किटेक्चर में विश्वसनीय बिल्डिंग ब्लॉक्स के रूप में उपयोग के लिए उच्च स्तर की विश्वसनीयता के पूर्व-परीक्षण वाले घटकों की एक लाइब्रेरी बनाना है। इस लाइब्रेरी में सुरक्षा पैटर्न शामिल हो सकते हैं (जैसे कि इनपुट डेटा की कीटाणुशोधन, आउटपुट फिल्टर, गोपनीयता और रनटाइम मॉनिटर) उच्च स्तर के विनिर्देशों से संभावित रूप से उत्पन्न होते हैं, साथ ही साथ बुनियादी ढांचे के घटक जैसे पुन: प्रयोज्य क्रिप्टो मॉड्यूल, कुंजी भंडारण, फ़ाइल सिस्टम, आदि। अत्यधिक विश्वसनीय नेटवर्क स्टैक और ड्राइवर। यदि सुरक्षा ऐसे एक से अधिक घटकों पर निर्भर करती है, तो उनकी सहभागिता और साझाकरण की विश्वसनीयता को उचित ठहराने की आवश्यकता है। यहां मुख्य तकनीकी समस्याएं संगामिति और प्रोटोकॉल के साथ-साथ विश्वसनीय घटकों की उपस्थिति में सूचना प्रवाह के बारे में चर्चा कर रही हैं। इन सीमाओं के बावजूद, काम seL4 पर आधारित वास्तविक अत्यधिक विश्वसनीय प्रणालियों के तेजी से विकास को दर्शाता है। वर्तमान में, पारंपरिक परीक्षण की तुलना में कम लागत पर ऐसी प्रणालियों का निर्माण संभव है।

आवेदन: श्रम लागत

SeL4 के लिए डिजाइन और कोड के विकास में दो मानव-वर्ष लगे। यदि हम सभी सीरोटाइप-विशिष्ट साक्ष्य जोड़ते हैं, तो सी के लिए कोड की 8700 लाइनों के लिए कुल 18 व्यक्ति-वर्ष प्राप्त किए जाएंगे। तुलनात्मक रूप से, एक तुलनीय आकार के माइक्रोकर्ल L4Ka का विकास :: सीतल परिवार के पिस्ता ने छह मानव-वर्ष लिए और विश्वसनीयता का एक महत्वपूर्ण स्तर प्रदान नहीं किया। इसका अर्थ है सत्यापित और पारंपरिक सॉफ़्टवेयर के बीच केवल 3.3 गुना की विकास गति में अंतर। कोलबर्ट और बोहम मूल्यांकन पद्धति के अनुसार, सी कोड की 8700 लाइनों के लिए पारंपरिक EAL7 मानदंडों के अनुसार 45.9 व्यक्ति-वर्ष से अधिक समय लगेगा। इसका मतलब यह है कि द्विआधारी स्तर पर कार्यान्वयन का औपचारिक सत्यापन पहले से ही सामान्य मानदंडों के अनुसार प्रमाणन के उच्चतम स्तर से 2.3 गुना सस्ता है, जबकि काफी अधिक विश्वसनीयता प्रदान करता है।

तुलना के लिए, यहां वर्णित एचएसीएमएस दृष्टिकोण प्रत्येक नई प्रणाली के लिए केवल मौजूदा साक्ष्य का उपयोग करता है, जिसमें उपकरण द्वारा उत्पन्न साक्ष्य भी शामिल है। इस प्रकार, इस दृष्टिकोण से मेल खाने वाली प्रणाली के लिए सामान्य प्रमाण प्रयास वर्षों तक नहीं, बल्कि मान-सप्ताह तक नीचे आता है और मान्यताओं को मान्य करने के लिए परीक्षण नीचे आता है।