Nadácia RISC-V o overení fungovania mikrojadra na systémoch s architektúrou inštrukčnej sady RISC-V. Overenie prichádza na rad spoľahlivosť prevádzky seL4, čo znamená úplný súlad so špecifikáciami uvedenými vo formálnom jazyku. Dôkaz o spoľahlivosti seL4 v kritických systémoch založených na procesoroch RISC-V RV64, ktoré vyžadujú zvýšenú úroveň spoľahlivosti a zaručujú absenciu porúch. Vývojári softvéru bežiaceho na jadre seL4 si môžu byť úplne istí, že ak dôjde k zlyhaniu v jednej časti systému, toto zlyhanie sa nerozšíri do zvyšku systému a najmä do jeho kritických častí.
Mikrokernel seL4 bol spočiatku overený pre 32-bitové procesory ARM a neskôr pre 64-bitové x86 procesory. Je potrebné poznamenať, že kombináciou otvorenej hardvérovej architektúry RISC-V s otvoreným mikrokernelom seL4 sa dosiahne nová úroveň bezpečnosti, pretože hardvérové komponenty môžu byť v budúcnosti plne overené, čo nie je možné dosiahnuť pre proprietárne hardvérové architektúry.
Pri overovaní seL4 sa predpokladá, že zariadenie funguje tak, ako je uvedené a špecifikácia plne popisuje správanie systému, ale v skutočnosti zariadenie nie je bez chýb, čo jasne dokazujú pravidelne sa objavujúce problémy v mechanizme špekulatívneho vykonávania inštrukcie. Otvorené hardvérové platformy uľahčujú integráciu zmien súvisiacich s bezpečnosťou – napríklad blokovanie všetkých možných únikov z bočných kanálov, kde je oveľa efektívnejšie zbaviť sa problému v hardvéri, ako sa snažiť nájsť riešenia v softvéri.
Pripomeňme, že architektúra seL4 presúvanie častí na riadenie zdrojov jadra do užívateľského priestoru a aplikovanie rovnakých prostriedkov riadenia prístupu pre také zdroje ako pre užívateľské zdroje. Mikrokernel neposkytuje hotové abstrakcie na vysokej úrovni pre správu súborov, procesov, sieťových pripojení a podobne, namiesto toho poskytuje len minimálne mechanizmy na riadenie prístupu k fyzickému adresnému priestoru, prerušeniam a zdrojom procesora. Vysokoúrovňové abstrakcie a ovládače pre interakciu s hardvérom sú implementované oddelene na vrchole mikrojadra vo forme úloh na užívateľskej úrovni. Prístup takýchto úloh k zdrojom dostupným pre mikrokernel je organizovaný prostredníctvom definície pravidiel.
RISC-V poskytuje otvorený a flexibilný systém strojových inštrukcií, ktorý umožňuje zostavenie mikroprocesorov pre ľubovoľné aplikácie bez toho, aby sa vyžadovali licenčné poplatky alebo reťazce. RISC-V vám umožňuje vytvárať úplne otvorené SoC a procesory. V súčasnosti vychádza zo špecifikácie RISC-V rôznymi spoločnosťami a komunitami pod rôznymi bezplatnými licenciami (BSD, MIT, Apache 2.0) niekoľko desiatok variant jadier mikroprocesorov, SoC a už vyrábaných čipov. Podpora RISC-V je prítomná od vydania Glibc 2.27, binutils 2.30, gcc 7 a linuxového jadra 4.15.
Zdroj: opennet.ru