Fundacija RISC-V je objavila, da je preverila funkcionalnost mikrojedra seL4 na sistemih z arhitekturo nabora ukazov RISC-V . Postopek preverjanja je zreduciran na matematični dokaz zanesljivosti seL4, kar kaže na popolno skladnost s specifikacijami, opredeljenimi v formalnem jeziku.
Preizkus zanesljivosti omogoča uporabo seL4 v kritičnih sistemih, ki temeljijo na procesorjih RV64 RISC-V , ki zahtevajo višjo raven zanesljivosti in ne zagotavljajo okvar.
Razvijalci programske opreme, ki se izvajajo na vrhu jedra seL4, so lahko popolnoma prepričani, da se v primeru okvare enega dela sistema ta okvara ne bo razširila na preostali del sistema in zlasti na njegove kritične dele.
O seL4
Arhitektura seL4 je znana po tem, da iz uporabniškega prostora odstrani dele za upravljanje virov jedra in uporabi enakih metod nadzora dostopa za te vire kot za uporabniške vire.
Mikrojedro ne ponuja že pripravljenih visokonivojskih abstrakcij za upravljanje datotek, procesov, omrežnih povezav itd., temveč le minimalne mehanizme za nadzor dostopa do fizičnega naslovnega prostora , prekinitev in procesorskih virov.
Vrhunske abstrakcije in krmilniki za interakcijo z računalnikom so nameščeni ločeno na mikrojedru v obliki nalog, ki se izvajajo na uporabniški ravni.
Dostop takšnih nalog do virov, ki so na voljo v mikrojedru, je organiziran z opredelitvijo pravil.
RISC-V zagotavlja odprt in prilagodljiv sistem strojnih ukazov, ki omogoča ustvarjanje mikroprocesorjev za poljubne aplikacije, brez potrebe po odbitkih in brez nalaganja pogojev uporabe.
RISC-V vam omogoča ustvarjanje popolnoma odprtih procesorjev in SoC-jev. Trenutno na podlagi specifikacije RISC-V več podjetij in skupnosti z različnimi brezplačnimi licencami (BSD, MIT, Apache 2.0) razvija več deset različic že izdelanih mikroprocesorskih jeder, SoC-jev in čipov.
Podpora za RISC-V obstaja že od izdaje Glibc 2.27, binutils 2.30, gcc 7 in jedra Linux 4.15.
O preizkušanju mikrojedr seL4
Sprva je bilo mikrojedro seL4 preverjeno za 32-bitne procesorje ARM , kasneje pa za 64-bitne procesorje x86.
Ugotovljeno je bilo, da bo kombinacija odprte strojne arhitekture RISC-V z odprtim mikrojedrom seL4 dosegla novo raven varnosti , saj bo mogoče strojne komponente v prihodnosti v celoti preveriti, kar je pri lastniških strojnih arhitekturah nemogoče doseči.
Ko preverjamo seL4, moramo domnevati, da strojna oprema deluje pravilno (torej, kot je določeno). To predpostavlja, da je najprej nedvoumna specifikacija, kar pa ne velja za vso strojno opremo.
Toda tudi če takšna specifikacija obstaja in je formalna (to je ritten v matematičnem formalizmu, ki podpira matematično sklepanje o svojih lastnostih), kako vemo, da dejansko zajema vedenje strojne opreme?
Resničnost je taka, da smo lahko povsem prepričani, da temu ni tako. Strojna oprema se ne razlikuje od programske opreme po tem, ker sta obe napačni.
Toda odprt ISA ima prednosti, ki presegajo brezplačnost. Eno je, da omogoča odprtokodne izvedbe strojne opreme.
Pri preverjanju seL4 se domneva, da oprema deluje, kot je navedeno, in specifikacija v celoti opisuje vedenje sistema, vendar v resnici oprema ni brez napak, kar dobro dokazujejo težave, ki se redno pojavljajo v navodilih špekulativnega izvršilnega mehanizma .
Odprte strojne platforme poenostavljajo integracijo sprememb, povezanih z varnostjo, na primer za blokiranje vseh možnih kanalov puščanja prek kanalov tretjih oseb, kjer je veliko učinkoviteje odpraviti težavo s strojno opremo kot pa poskušati najti rešitve s programsko opremo.
Nazadnje, če želite izvedeti več o tem, si lahko članek ogledate na naslednji povezavi.