seL4 mikrokern wiskundig geverifieer vir RISC-V argitektuur

RISC-V-stigting berig oor die verifiëring van die werking van die mikrokern seL4 op stelsels met RISC-V instruksiestel argitektuur. Verifikasie kom neer op wiskundige bewys betroubaarheid van seL4-werking, wat volledige voldoening aan die spesifikasies in die formele taal aandui. Bewys van betroubaarheid laat jou toe om te gebruik seL4 in missiekritieke stelsels gebaseer op RISC-V RV64 verwerkers wat 'n verhoogde vlak van betroubaarheid vereis en die afwesigheid van mislukkings waarborg. Ontwikkelaars van sagteware wat bo-op die seL4-kern loop, kan heeltemal vol vertroue wees dat indien daar 'n fout in een deel van die stelsel is, hierdie mislukking nie na die res van die stelsel en veral sy kritieke dele sal versprei nie.

Die seL4-mikrokern is aanvanklik vir 32-bis ARM-verwerkers geverifieer, en later vir 64-bis x86-verwerkers. Daar word kennis geneem dat die kombinasie van die oop RISC-V hardeware argitektuur met die oop seL4 mikrokern 'n nuwe vlak van sekuriteit sal bereik, aangesien die hardeware komponente ook volledig geverifieer kan word in die toekoms, wat onmoontlik is om te bereik vir eie hardeware argitekture.

При верификации seL4 предполагается, что оборудование работает как заявлено и спецификация полностью описывает поведение системы, но на деле оборудование не избавлено от ошибок, что хорошо демонстрируется всплывающими регулярно проблемами в механизме спекулятивного выполнения инструкций. Open hardware platforms simplify the integration of changes related to safety - for example, to block all possible leakage channels by third -party channels, in which it is much more efficient to get rid of the problem of hardware than trying to look for bypass tracks programmatically .

Onthou dat die seL4-argitektuur merkwaardig bewegende dele vir die bestuur van kernhulpbronne in gebruikersruimte en die toepassing van dieselfde toegangsbeheermiddele vir sulke hulpbronne as vir gebruikershulpbronne. Die mikrokern verskaf nie klaargemaakte hoëvlak-abstraksies vir die bestuur van lêers, prosesse, netwerkverbindings en dies meer nie; in plaas daarvan bied dit slegs minimale meganismes om toegang tot fisiese adresruimte, onderbrekings en verwerkerhulpbronne te beheer. Hoëvlak-abstraksies en drywers vir interaksie met hardeware word afsonderlik bo-op die mikrokern geïmplementeer in die vorm van gebruikersvlaktake. Toegang van sulke take tot die hulpbronne beskikbaar vir die mikrokern word georganiseer deur die definisie van reëls.

RISC-V bied 'n oop en buigsame masjieninstruksiestelsel wat dit moontlik maak om mikroverwerkers vir arbitrêre toepassings te bou sonder dat tantieme of stringe aan gebruik vereis word. Met RISC-V kan u heeltemal oop SoC's en verwerkers skep. Tans gebaseer op die RISC-V-spesifikasie deur verskillende maatskappye en gemeenskappe onder verskeie gratis lisensies (BSD, MIT, Apache 2.0) ontwikkel verskeie dosyn variante van mikroverwerker-kerne, SoC's en reeds vervaardigde skyfies. RISC-V-ondersteuning is teenwoordig sedert die vrystellings van Glibc 2.27, binutils 2.30, gcc 7 en die Linux-kern 4.15.

Bron: opennet.ru