SeL4 माइक्रोकर्नेल को RISC-V आर्किटेक्चर के लिए गणितीय रूप से सत्यापित किया गया है

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

एसईएल4 माइक्रोकर्नेल को शुरुआत में 32-बिट एआरएम प्रोसेसर के लिए और बाद में 64-बिट x86 प्रोसेसर के लिए सत्यापित किया गया था। यह ध्यान दिया जाता है कि खुले आरआईएससी-वी हार्डवेयर आर्किटेक्चर का खुले एसईएल4 माइक्रोकर्नेल के साथ संयोजन सुरक्षा के एक नए स्तर को प्राप्त करेगा, क्योंकि भविष्य में हार्डवेयर घटकों को भी पूरी तरह से सत्यापित किया जा सकता है, जो मालिकाना हार्डवेयर आर्किटेक्चर के लिए हासिल करना असंभव है।

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

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

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

स्रोत: opennet.ru