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

RISC-V फाउन्डेसन रिपोर्ट गरियो microkernel को सञ्चालन प्रमाणीकरण बारे seL4 RISC-V निर्देशन सेट वास्तुकला संग प्रणालीहरूमा। प्रमाणीकरण तल आउँछ गणितीय प्रमाण seL4 सञ्चालनको विश्वसनीयता, जसले औपचारिक भाषामा निर्दिष्ट विनिर्देशहरूको पूर्ण अनुपालनलाई संकेत गर्दछ। विश्वसनीयता को प्रमाण प्रयोग गर्न अनुमति दिन्छ RISC-V RV4 प्रोसेसरहरूमा आधारित मिशन-क्रिटिकल प्रणालीहरूमा seL64 जसलाई विश्वसनीयताको बढ्दो स्तर चाहिन्छ र विफलताहरूको अनुपस्थितिको ग्यारेन्टी गर्दछ। seL4 कर्नेलको माथि चलिरहेको सफ्टवेयरका विकासकर्ताहरू पूर्णतया विश्वस्त हुन सक्छन् कि यदि प्रणालीको एक भागमा विफलता छ भने, यो विफलता प्रणालीको बाँकी भागहरूमा फैलिने छैन र विशेष गरी, यसको महत्वपूर्ण भागहरूमा।

seL4 माइक्रोकर्नेल प्रारम्भमा 32-bit ARM प्रोसेसरहरूको लागि प्रमाणित गरिएको थियो, र पछि 64-bit 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