RISC-V Alapítvány a mikrokernel működésének ellenőrzéséről RISC-V utasításkészlet architektúrájú rendszereken. Az ellenőrzés lényege a seL4 működésének megbízhatósága, ami a hivatalos nyelvben meghatározott előírásoknak való teljes megfelelést jelzi. A megbízhatóság igazolása seL4 RISC-V RV64 processzorokon alapuló, kritikus rendszerekben, amelyek fokozott megbízhatóságot igényelnek, és garantálják a hibák elkerülését. A seL4 kernel tetején futó szoftverek fejlesztői teljesen biztosak lehetnek abban, hogy ha a rendszer egy részében meghibásodás történik, ez a hiba nem terjed át a rendszer többi részére, és különösen annak kritikus részeire.
A seL4 mikrokernelt kezdetben 32 bites ARM processzorokhoz, majd később 64 bites x86 processzorokhoz ellenőrizték. Megjegyzendő, hogy a nyitott RISC-V hardverarchitektúra és a nyitott seL4 mikrokernellel való kombinációja a biztonság új szintjét éri el, mivel a hardverkomponensek a jövőben is teljes körűen ellenőrizhetők, ami a szabadalmaztatott hardverarchitektúrák esetében lehetetlen.
A seL4 ellenőrzésekor feltételezzük, hogy a berendezés a leírtak szerint működik, és a specifikáció teljes mértékben leírja a rendszer viselkedését, de a valóságban a berendezés nem mentes a hibáktól, amit egyértelműen mutatnak a spekulatív végrehajtás mechanizmusában rendszeresen felmerülő problémák. utasítás. A nyílt hardverplatformok megkönnyítik a biztonsággal kapcsolatos változtatások integrálását – például blokkolják az összes lehetséges oldalcsatornás szivárgást, ahol sokkal hatékonyabb a hardveres probléma megoldása, mint szoftveres megoldások keresése.
Emlékezzünk arra, hogy a seL4 architektúra a kernel erőforrások kezeléséhez szükséges alkatrészeket mozgatja a felhasználói térbe, és ugyanazokat a hozzáférés-vezérlési eszközöket alkalmazza az ilyen erőforrásokhoz, mint a felhasználói erőforrásokhoz. A mikrokernel nem ad kész magas szintű absztrakciókat a fájlok, folyamatok, hálózati kapcsolatok és hasonlók kezelésére, ehelyett csak minimális mechanizmusokat biztosít a fizikai címtérhez, a megszakításokhoz és a processzorerőforrásokhoz való hozzáférés szabályozására. A magas szintű absztrakciók és a hardverrel való interakcióhoz szükséges illesztőprogramok külön vannak implementálva a mikrokernel tetején, felhasználói szintű feladatok formájában. Az ilyen feladatoknak a mikrokernel rendelkezésére álló erőforrásokhoz való hozzáférése szabályok meghatározásán keresztül történik.
A RISC-V nyílt és rugalmas gépi utasításrendszert biztosít, amely lehetővé teszi mikroprocesszorok tetszőleges alkalmazásokhoz való építését anélkül, hogy jogdíjakat vagy láncokat kellene használnia. A RISC-V lehetővé teszi teljesen nyitott SoC-ok és processzorok létrehozását. Jelenleg a különböző vállalatok és közösségek RISC-V specifikációján alapul, különböző ingyenes licencek (BSD, MIT, Apache 2.0) alatt. mikroprocesszormagok, SoC-k és már gyártott chipek több tucat változata. A RISC-V támogatás a Glibc 2.27, a binutils 2.30, a gcc 7 és a Linux kernel 4.15 kiadása óta létezik.
Forrás: opennet.ru