Nadácia RISC-V oznámila, že overila funkčnosť mikrojadra seL4 na systémoch s architektúrou inštrukčnej sady RISC-V . Proces overovania sa redukuje na matematický dôkaz spoľahlivosti seL4, čo naznačuje úplný súlad so špecifikáciami definovanými vo formálnom jazyku.
Test spoľahlivosti umožňuje použitie seL4 v kritických systémoch založených na procesoroch RV64 RISC-V , ktoré vyžadujú vyššiu úroveň spoľahlivosti a nezaručuje poruchy.
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í pre správu zdrojov jadra z používateľského priestoru a použitím rovnakých metód riadenia prístupu pre tieto zdroje ako pre používateľské zdroje.
Mikrojadro neposkytuje hotové abstrakcie na vysokej úrovni na správu súborov, procesov, sieťových pripojení atď., ale poskytuje iba minimálne mechanizmy na riadenie prístupu k fyzickému adresnému priestoru , prerušeniam a procesorovým zdrojom.
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 inštrukcií, ktorý umožňuje vytváranie mikroprocesorov pre ľubovoľné aplikácie bez nutnosti odvodzovania 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
Mikrojadro seL4 bolo spočiatku overené pre 32-bitové procesory ARM a neskôr pre 64-bitové procesory x86.
Pozoruje sa, že kombinácia otvorenej hardvérovej architektúry RISC-V s otvoreným mikrojadrom seL4 dosiahne novú úroveň bezpečnosti , pretože hardvérové komponenty bude možné v budúcnosti plne overiť, čo je nemožné dosiahnuť pri proprietárnych hardvérových architektúrach.
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 súvisiacich s bezpečnosťou, napríklad blokujú všetky možné úniky informácií prostredníctvom kanálov tretích strán, kde je oveľa efektívnejšie zbaviť sa problému hardvérom, ako sa snažiť nájsť riešenia softvérom.
Na záver, ak sa chcete dozvedieť viac, môžete si prečítať článok na nasledujúcom odkaze.