RISC-V ने अपने RV4 प्रोसेसर पर seL64 माइक्रोकर्नेल को सत्यापित किया

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

विश्वसनीयता परीक्षण RLC-V प्रोसेसर के आधार पर seL4 को मिशन महत्वपूर्ण प्रणालियों में उपयोग करने में सक्षम बनाता है RV64, जिसे उच्च स्तर की विश्वसनीयता की आवश्यकता होती है और विफलता की गारंटी नहीं देता है।

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

SeL4 के बारे में

SeL4 वास्तुकला उपयोगकर्ता स्थान में कर्नेल संसाधनों को प्रबंधित करने के लिए भागों को हटाने के लिए उल्लेखनीय है और उपयोगकर्ता संसाधनों के लिए ऐसे संसाधनों के लिए समान अभिगम नियंत्रण विधियों का उपयोग करें।

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

कंप्यूटर के साथ बातचीत करने के लिए उच्च-स्तरीय अमूर्त और नियंत्रक को उपयोगकर्ता के स्तर पर किए गए कार्यों के रूप में माइक्रोक्रेन के शीर्ष पर अलग से लागू किया जाता है।

माइक्रोकर्नेल में उपलब्ध संसाधनों तक ऐसे कार्यों की पहुंच नियमों की परिभाषा के माध्यम से आयोजित की जाती है।

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

RISC-V आपको पूरी तरह से खुले प्रोसेसर और SoCs बनाने की अनुमति देता है। वर्तमान में, आरआईएससी-वी विनिर्देश के आधार पर, कई कंपनियों और समुदायों ने विभिन्न मुफ्त लाइसेंस (बीएसडी, एमआईटी, अपाचे 2.0) के तहत पहले से उत्पादित माइक्रोप्रोसेसर कोर, SoCs और चिप्स के कई दर्जन वेरिएंट विकसित कर रहे हैं।

RISC-V का समर्थन ग्लिबेक 2.27, बिनुटिल्स 2.30, gcc 7 और लिनक्स 4.15 कर्नेल के रिलीज़ होने के बाद से है।

SeL4 माइक्रोकर्नल परीक्षण के बारे में

प्रारंभ में, माइक्रोकर्नेल seL4 को 32-बिट ARM प्रोसेसर के लिए सत्यापित किया गया था, और बाद में x86 64-बिट प्रोसेसर के लिए.

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

जब हम seL4 की जांच करते हैं, तो हमें यह मान लेना चाहिए कि हार्डवेयर ठीक से काम कर रहा है (जैसा कि निर्दिष्ट है)। यह मानते हैं कि पहली जगह में एक स्पष्ट विनिर्देश है, जो सभी हार्डवेयर के लिए नहीं है। 

लेकिन यहां तक ​​कि जब इस तरह के विनिर्देश मौजूद हैं, और यह औपचारिक है (जो कि गणितीय औपचारिकता में लिखा गया है, जो इसके गुणों के बारे में गणितीय तर्क का समर्थन करता है), हम कैसे जानते हैं कि यह वास्तव में हार्डवेयर के व्यवहार को पकड़ता है? 

वास्तविकता यह है कि हम यह सुनिश्चित कर सकते हैं कि यह नहीं है। हार्डवेयर सॉफ्टवेयर से अलग नहीं है, दोनों ही छोटी गाड़ी हैं।

लेकिन आईएसए के खुले होने के फायदे हैं जो रॉयल्टी-फ्री होने से परे हैं। एक यह है कि यह खुले स्रोत हार्डवेयर कार्यान्वयन की अनुमति देता है।

SeL4 की जाँच करते समय, यह माना जाता है कि उपकरण संकेत के अनुसार काम करता है और विनिर्देश पूरी तरह से सिस्टम के व्यवहार का वर्णन करता है, लेकिन वास्तव में उपकरण त्रुटि मुक्त नहीं है, जो कि समस्याओं से अच्छी तरह से प्रदर्शित होता है जो नियमित रूप से सट्टा निष्पादन तंत्र में उत्पन्न होते हैं। ।

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

अंत में, यदि आप इसके बारे में अधिक जानना चाहते हैं, तो आप नोट को परामर्श कर सकते हैं निम्नलिखित लिंक।