RISC-V Alapítvány a mikrokernel működésének verifikációjáról RISC-V utasításkészlet architekturájú rendszereken. A verifikáció lényege a seL4 megbízhatóságának, amely tanúsítja a formális nyelven megfogalmazott specifikációknak való teljes megfelelést. A megbízhatóság bizonyítása a seL4 használatát kritikus fontosságú RISC-V RV64 processzorokra épülő rendszerekben, amelyeket megnövelt megbízhatósági szint igényel, és garantálja a meghibásodások hiányát. A seL4 kernelen működő szoftverfejlesztők teljesen biztosak lehetnek abban, hogy ha a rendszer egyik részében hiba lép fel, ez a hiba nem terjed át a rendszer többi részére, különösen a kritikus részekre.
Eredetileg a seL4 mikrokernel 32-bites ARM folyamatorkezelőkhöz volt verifikálva, később pedig 64-bites x86 folyamatorkezelőkhöz. Megjegyzendő, hogy a RISC-V nyílt hardverarchitektúra és a nyílt seL4 mikrokernel kombinációja új szintű biztonságot eredményez, mivel a hardverkomponensek a jövőben teljes mértékben verifikálhatók lesznek, ami nem lehetséges a zárt hardverarchitektúrák esetében.
A seL4 verifikációja során feltételezzük, hogy a hardver a megadott módon működik, és a specifikáció teljes mértékben leírja a rendszer viselkedését, de valójában a hardver nem mentes a hibáktól, amit jól mutatnak a spekulatív utasításvégrehajtás mechanizmusával kapcsolatos problémák, amelyek rendszeresen felbukkannak. A nyílt hardverplatformok egyszerűsítik a biztonsággal kapcsolatos változtatások integrálását – például az összes lehetséges szivárgási csatorna lezárására, ahol sokkal hatékonyabb a problémát hardveresen megszüntetni, mint szoftveres kerülőutakat keresni.
Emlékeztetőül, a seL4 architektúra A kernel microkernel abstracts management parts into user space and employs similar access control mechanisms for these resources as for user resources. The microkernel does not provide ready-made high-level abstractions for managing files, processes, network connections, etc.; instead, it offers only minimal mechanisms for accessing physical address space, handling interrupts, and CPU resources. High-level abstractions and drivers for interacting with hardware are implemented separately on top of the microkernel as tasks executed at the user level. Access to the resources available to the microkernel by these tasks is organized through the definition of rules.
A RISC-V nyílt és rugalmas gépi utasítások rendszere, amely lehetővé teszi különféle alkalmazású mikroprocesszorok létrehozását, miközben nem igényel díjakat és nem támaszt használati feltételeket. A RISC-V lehetővé teszi teljesen nyílt SoC-k és processzorok létrehozását. Jelenleg a RISC-V specifikáción alapuló különböző cégek és közösségek által különböző nyílt licencjogok (BSD, MIT, Apache 2.0) alatt több tucatnyi mikroprocesszor-architektúrát, SoC-t és már előállított chipet támogatnak. A RISC-V támogatása a Glibc 2.27, a binutils 2.30, a gcc 7 és a Linux 4.15 verziók megjelenésével kezdődött.
Forrás: opennet.ru
