Organizace RISC-V Foundation o verifikaci mikrokernelů v systémech s architekturou instrukčního setu RISC-V. Verifikace se soustředí na spolehlivosti seL4, který potvrzuje úplnou shodu se specifikacemi zadanými ve formálním jazyce. Důkaz spolehlivosti seL4 v kritických systémech založených na procesorech RISC-V RV64, které vyžadují vyšší úroveň spolehlivosti a garantují absenci selhání. Vývojáři softwaru běžícího na jádře seL4 si mohou být zcela jisti, že v případě selhání jedné části systému se toto selhání nešíří na zbytek systému a zejména na jeho kritické části.
Původně byl mikrokernel seL4 verifikován pro 32bitové procesory ARM a později pro 64bitové procesory x86. Je zdůrazněno, že kombinace otevřené hardwarové architektury RISC-V s otevřeným mikrokernelem seL4 umožní dosáhnout nové úrovně zabezpečení, protože hardwarové komponenty mohou být také plně verifikovány, což není možné u proprietárních hardwarových architektur.
Při verifikaci seL4 se předpokládá, že hardware funguje, jak bylo prohlášeno, a specifikace plně popisuje chování systému, ale ve skutečnosti hardware není bez chyb, což je dobře ukázáno pravidelně se objevujícími problémy v mechanismu spekulativního vykonávání instrukcí. Otevřené hardwarové platformy usnadňují integraci změn souvisejících s bezpečností - například pro zablokování všech možných kanálů úniků přes externí kanály, kde je mnohem efektivnější vyřešit problém hardwarově než se pokoušet hledat softwarové obchvaty.
Připomeňme, že architektura seL4 vyjmutí částí pro řízení prostředků jádra do prostoru uživatele a použití pro tyto prostředky stejných prostředků přístupu, jaké se používají pro uživatelské prostředky. Mikrojádro neposkytuje hotové vysoceúrovňové abstrakce pro správu souborů, procesů, síťových spojení atd., místo toho poskytuje pouze minimální mechanismy pro řízení přístupu k fyzickému adresnímu prostoru, přerušení a prostředkům procesoru. Vysoceúrovňové abstrakce a ovladače pro interakci s hardwarem jsou implementovány odděleně nad mikrojádrem ve formě úloh vykonávaných na uživatelské úrovni. Přístup těchto úloh k prostředkům, které má mikrojádro k dispozici, je organizován prostřednictvím definice pravidel.
RISC-V poskytuje otevřený a flexibilní systém strojových instrukcí, který umožňuje vytvářet mikroprocesory pro libovolné oblasti použití, aniž by vyžadoval licenční poplatky a neukládal podmínky pro použití. RISC-V umožňuje vytvářet zcela otevřené SoC a procesory. V současné době je na základě specifikace RISC-V různými společnostmi a komunitami pod různými otevřenými licencemi (BSD, MIT, Apache 2.0) k dispozici několik desítek variant jader mikroprocesorů, SoC a již vyráběných čipů. Podpora RISC-V je přítomna od verzí Glibc 2.27, binutils 2.30, gcc 7 a jádra Linux 4.15. Release zvukového subsystému Linux — ALSA 1.2.3
Zdroj: opennet.ru
