RISC-V फाउंडेशन मायक्रोकर्नलच्या ऑपरेशनची पडताळणी करण्याबद्दल RISC-V इंस्ट्रक्शन सेट आर्किटेक्चर असलेल्या सिस्टमवर. वर पडताळणी खाली येते seL4 ऑपरेशनची विश्वासार्हता, जे औपचारिक भाषेत निर्दिष्ट केलेल्या वैशिष्ट्यांचे पूर्ण पालन दर्शवते. विश्वासार्हतेचा पुरावा RISC-V RV4 प्रोसेसरवर आधारित मिशन-क्रिटिकल सिस्टीममध्ये seL64 ज्यांना विश्वासार्हतेची वाढीव पातळी आवश्यक आहे आणि अपयशाच्या अनुपस्थितीची हमी आहे. seL4 कर्नलच्या वर चालणार्‍या सॉफ्टवेअरचे विकसक पूर्ण विश्वास ठेवू शकतात की सिस्टमच्या एका भागात बिघाड झाल्यास, हे अपयश उर्वरित सिस्टममध्ये आणि विशेषतः, त्याच्या गंभीर भागांमध्ये पसरणार नाही.
seL4 मायक्रोकर्नल सुरुवातीला 32-बिट एआरएम प्रोसेसरसाठी आणि नंतर 64-बिट x86 प्रोसेसरसाठी सत्यापित केले गेले. ओपन seL4 मायक्रोकर्नलसह ओपन RISC-V हार्डवेअर आर्किटेक्चरचे संयोजन सुरक्षिततेचा एक नवीन स्तर प्राप्त करेल, कारण भविष्यात हार्डवेअर घटक देखील पूर्णपणे सत्यापित केले जाऊ शकतात, जे मालकी हार्डवेअर आर्किटेक्चरसाठी साध्य करणे अशक्य आहे.
seL4 ची पडताळणी करताना, असे गृहीत धरले जाते की उपकरणे सांगितल्याप्रमाणे कार्य करतात आणि तपशील प्रणालीच्या वर्तनाचे पूर्णपणे वर्णन करतात, परंतु प्रत्यक्षात उपकरणे त्रुटींपासून मुक्त नाहीत, जे सट्टा अंमलबजावणीच्या यंत्रणेमध्ये नियमितपणे उद्भवणाऱ्या समस्यांद्वारे स्पष्टपणे दिसून येते. सूचना. ओपन हार्डवेअर प्लॅटफॉर्ममुळे सुरक्षितता-संबंधित बदल एकत्रित करणे सोपे होते - उदाहरणार्थ, सर्व संभाव्य साइड-चॅनल लीक अवरोधित करणे, जेथे सॉफ्टवेअरमध्ये वर्कअराउंड शोधण्याचा प्रयत्न करण्यापेक्षा हार्डवेअरमधील समस्येपासून मुक्त होणे अधिक कार्यक्षम आहे.
seL4 आर्किटेक्चर लक्षात ठेवा कर्नल संसाधने वापरकर्त्याच्या जागेत व्यवस्थापित करण्यासाठी भाग हलवणे आणि वापरकर्ता संसाधनांसारख्या संसाधनांसाठी समान प्रवेश नियंत्रण साधन लागू करणे. मायक्रोकर्नल फाइल्स, प्रक्रिया, नेटवर्क कनेक्शन्स आणि यासारख्या व्यवस्थापित करण्यासाठी तयार उच्च-स्तरीय अॅब्स्ट्रॅक्शन प्रदान करत नाही; त्याऐवजी, ते भौतिक पत्ता स्थान, व्यत्यय आणि प्रोसेसर संसाधनांवर प्रवेश नियंत्रित करण्यासाठी फक्त किमान यंत्रणा प्रदान करते. हार्डवेअरशी संवाद साधण्यासाठी उच्च-स्तरीय अॅब्स्ट्रॅक्शन्स आणि ड्रायव्हर्स वापरकर्ता-स्तरीय कार्यांच्या स्वरूपात मायक्रोकर्नलच्या वर स्वतंत्रपणे लागू केले जातात. मायक्रोकर्नलकडे उपलब्ध असलेल्या संसाधनांमध्ये अशा कार्यांचा प्रवेश नियमांच्या व्याख्येद्वारे आयोजित केला जातो.
RISC-V एक खुली आणि लवचिक मशीन सूचना प्रणाली प्रदान करते जी मायक्रोप्रोसेसरना रॉयल्टी किंवा वापरासाठी जोडलेल्या स्ट्रिंगची आवश्यकता न ठेवता अनियंत्रित अनुप्रयोगांसाठी तयार करण्यास अनुमती देते. RISC-V तुम्हाला पूर्णपणे उघडे SoCs आणि प्रोसेसर तयार करण्यास अनुमती देते. सध्या विविध कंपन्या आणि समुदायांद्वारे विविध मोफत परवान्यांद्वारे (BSD, MIT, Apache 2.0) RISC-V तपशीलावर आधारित मायक्रोप्रोसेसर कोर, SoCs आणि आधीच उत्पादित चिप्सचे अनेक डझन प्रकार. RISC-V समर्थन Glibc 2.27, binutils 2.30, gcc 7, आणि Linux कर्नल 4.15 च्या प्रकाशनापासून उपस्थित आहे.
स्त्रोत: opennet.ru