RISC-V ověřil mikrokernel seL4 na jejich procesorech RV64

Nadace RISC-V oznámila, že ověřila jak funguje mikrokernel seL4 v systémech s architektura instrukční sady RISC-V. Ve kterém je proces ověřování redukován na matematický test spolehlivosti seL4, který naznačuje plný soulad se specifikacemi specifikovanými ve formálním jazyce.

Testování spolehlivosti umožňuje použití seL4 v kritických systémech založených na procesorech RISC-V RV64, který vyžaduje vyšší úroveň spolehlivosti a nezaručuje selhání.

Softwaroví vývojáři, kteří běží nad jádrem seL4, si mohou být zcela jisti, že v případě selhání v jedné části systému se tato chyba nerozšíří do zbytku systému, a zejména do jeho kritických částí.

O seL4

Architektura seL4 je pozoruhodné při odebírání částí pro správu prostředků jádra v uživatelském prostoru a použít stejné metody řízení přístupu pro takové prostředky jako pro uživatelské zdroje.

Mikrojádro neposkytuje abstrakce na vysoké úrovni již připraveni spravovat soubory, procesy, síťová připojení atd., ale místo toho poskytuje pouze minimální mechanismy pro řízení přístupu do prostoru fyzických adres, přerušení a prostředky procesoru.

Abstrakce na vysoké úrovni a řadiče pro interakci s počítačem jsou implementovány samostatně v horní části mikrokernelů ve formě úkolů prováděných na uživatelské úrovni.

Přístup těchto úkolů ke zdrojům dostupným v mikrokernelu je organizován prostřednictvím definice pravidel.

RISC-V poskytuje otevřený a flexibilní systém strojových pokynů, které umožňuje vytvářet mikroprocesory pro libovolné aplikace bez nutnosti odečtení a bez uložení podmínek používání.

RISC-V umožňuje vytvářet zcela otevřené procesory a SoC. V současné době na základě specifikace RISC-V vyvíjí několik společností a komunit pod různými bezplatnými licencemi (BSD, MIT, Apache 2.0) několik desítek variant již vyrobených mikroprocesorových jader, SoC a čipů.

Podpora RISC-V existuje od vydání Glibc 2.27, binutils 2.30, gcc 7 a jádra Linuxu 4.15.

O testování mikrokernelů seL4

Zpočátku microkernel seL4 byl ověřen pro 32bitové procesory ARMA později pro x86 64bitové procesory.

Je pozorováno, že kombinace otevřené hardwarové architektury RISC-V s otevřenou mikrokernelem seL4 dosáhne nové úrovně zabezpečeníprotože hardwarové komponenty lze v budoucnu také plně ověřit, čehož je u proprietárních hardwarových architektur nemožné dosáhnout.

Když zkontrolujeme seL4, musíme předpokládat, že hardware funguje správně (tj. Jak je uvedeno). To předpokládá, že na prvním místě je jednoznačná specifikace, což neplatí pro veškerý hardware. 

Ale i když taková specifikace existuje a je formální (tj. V matematickém formalismu, který podporuje matematické úvahy o jeho vlastnostech), jak víme, že ve skutečnosti zachycuje chování hardwaru? 

Realita je taková, že si můžeme být docela jisti, že tomu tak není. Hardware se neliší od softwaru v tom, že oba jsou buggy.

Ale mít otevřený ISA má výhody, které jdou nad rámec toho, že jsou bez licenčních poplatků. Jedním z nich je, že umožňuje hardwarové implementace open source.

Při kontrole seL4 se předpokládá, že zařízení pracuje tak, jak je uvedeno, a specifikace plně popisuje chování systému, ale ve skutečnosti není zařízení bezchybné, což dobře dokazují problémy, které se pravidelně objevují ve spekulativním mechanismu provádění Pokyny .

Otevřené hardwarové platformy zjednodušují integraci změn související s bezpečností, například blokovat všechny možné kanály úniku prostřednictvím kanálů třetích stran, kde je mnohem efektivnější zbavit se problému pomocí hardwaru, než se snažit hledat řešení pomocí softwaru.

Nakonec, pokud se o tom chcete dozvědět více, můžete si prostudovat poznámku v následující odkaz.