RISC-V overil mikrokernel seL4 na svojich procesoroch RV64

Nadácia RISC-V oznámila, že overila ako funguje mikrokernel seL4 v systémoch s architektúra inštrukčnej sady RISC-V. V ktorom sa proces overovania zníži na matematický dôkaz spoľahlivosti seL4, ktorý naznačuje úplný súlad so špecifikáciami špecifikovanými vo formálnom jazyku.

Testovanie spoľahlivosti umožňuje použitie seL4 v kritických systémoch založených na procesoroch RISC-V RV64, ktorá vyžaduje vyššiu úroveň spoľahlivosti a nezaručuje zlyhanie.

Softvéroví vývojári bežiaci na jadre seL4 si môžu byť úplne istí, že v prípade zlyhania jednej časti systému sa táto porucha nerozšíri do zvyšku systému a najmä do jeho kritických častí.

O seL4

Architektúra seL4 je pozoruhodný odstránením častí na správu prostriedkov jadra v užívateľskom priestore a používať rovnaké metódy riadenia prístupu pre také prostriedky ako pre užívateľské zdroje.

Mikrokernel neposkytuje abstrakcie na vysokej úrovni už pripravený na správu súborov, procesov, sieťových pripojení atď., ale namiesto toho poskytuje iba minimálne mechanizmy na riadenie prístupu do priestoru fyzických adries, prerušenia a prostriedky procesora.

Abstrakcie a ovládače na vysokej úrovni pre interakciu s počítačom sú implementované osobitne na vrchu mikrokernelu vo forme úloh vykonávaných na úrovni používateľa.

Prístup týchto úloh k zdrojom dostupným v mikrokerneli je organizovaný prostredníctvom definície pravidiel.

RISC-V poskytuje otvorený a flexibilný systém strojových pokynov, ktoré umožňuje vytvárať mikroprocesory pre ľubovoľné aplikácie bez toho, aby vyžadoval odpočty a bez stanovenia podmienok používania.

RISC-V umožňuje vytvárať úplne otvorené procesory a SoC. V súčasnosti na základe špecifikácie RISC-V niekoľko spoločností a komunít na základe rôznych bezplatných licencií (BSD, MIT, Apache 2.0) vyvíja niekoľko desiatok variantov už vyrobených mikroprocesorových jadier, SoC a čipov.

Podpora RISC-V existuje už od vydania Glibc 2.27, binutils 2.30, gcc 7 a jadra Linux 4.15.

O testovaní mikrojadier seL4

Spočiatku mikrokernel seL4 bol overený pre 32-bitové procesory ARMA neskôr pre x86 64-bitové procesory.

Pozorovalo sa, že kombinácia otvorenej hardvérovej architektúry RISC-V s otvoreným mikrojadrom seL4 dosiahne novú úroveň bezpečnosti, pretože budúce hardvérové ​​komponenty je tiež možné úplne overiť, čo je pre proprietárne hardvérové ​​architektúry nemožné.

Keď kontrolujeme seL4, musíme predpokladať, že hardvér funguje správne (to znamená, ako je uvedené). To predpokladá, že na prvom mieste je jednoznačná špecifikácia, čo neplatí pre všetok hardvér. 

Ale aj keď taká špecifikácia existuje a je formálna (to znamená, že je matematicky formalizovaná tak, že podporuje matematické úvahy o jej vlastnostiach), ako vieme, že vlastne zachytáva správanie hardvéru? 

Realita je taká, že si môžeme byť celkom istí, že to tak nie je. Hardvér sa nijako nelíši od softvéru v tom, že oba sú buggy.

Ale mať otvorený ISA má výhody, ktoré presahujú rámec bez poplatkov. Jedným z nich je, že umožňuje hardvérové ​​implementácie otvoreného zdroja.

Pri kontrole seL4 sa predpokladá, že zariadenie pracuje podľa pokynov a v špecifikácii je úplne popísané chovanie systému, ale v skutočnosti nie je bezchybné, čo dobre dokazujú problémy, ktoré sa pravidelne vyskytujú v špekulatívnom mechanizme vykonania. Pokyny .

Otvorené hardvérové ​​platformy zjednodušujú integráciu zmien v súvislosti s bezpečnosťou napríklad blokovanie všetkých možných kanálov úniku prostredníctvom kanálov tretích strán, kde je oveľa efektívnejšie zbaviť sa problému pomocou hardvéru, ako sa pokúšať hľadať riešenia pomocou softvéru.

Nakoniec, ak sa o tom chcete dozvedieť viac, môžete si prečítať poznámku v nasledujúci odkaz.