RISC-V je preveril mikrojedro seL4 na svojih procesorjih RV64

Fundacija RISC-V je sporočila, da je preverila kako mikrojedrce deluje seL4 v sistemih z arhitektura nabora navodil RISC-V. V katerem se postopek preverjanja zmanjša na matematični dokaz zanesljivosti seL4, kar kaže na popolno skladnost s specifikacijami, določenimi v formalnem jeziku.

Preizkus zanesljivosti omogoča uporabo seL4 v kritičnih sistemih, ki temeljijo na procesorjih RISC-V RV64, ki zahteva višjo stopnjo zanesljivosti in ne zagotavlja okvare.

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 opazen po odstranitvi delov za upravljanje virov jedra v uporabniškem prostoru in za take vire uporabljajte enake metode nadzora dostopa kot za uporabniške vire.

Mikrojedro ne zagotavlja abstrakcij na visoki ravni že pripravljen za upravljanje datotek, procesov, omrežnih povezav itd., ampak namesto tega ponuja le minimalne mehanizme za nadzor dostopa do fizičnega naslovnega prostora, prekinitve in viri procesorja.

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 navodil, ki omogoča ustvarjanje mikroprocesorjev za poljubne aplikacije, brez potrebe po odbitkih in brez postavljanja 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 mikrojedra seL4 je bil preverjen za 32-bitne procesorje ARM, In kasneje za x86 64-bitne procesorje.

Opazimo, da je kombinacija odprte strojne arhitekture RISC-V z odprtim mikrojedrom seL4 bo dosegel novo raven varnosti, saj je mogoče tudi prihodnje komponente strojne opreme v celoti preveriti, kar je za lastniške arhitekture strojne opreme 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 povezane z varnostjo, na primer z blokiranjem vseh možnih kanalov puščanja prek tujih kanalov, kjer je veliko bolj učinkovito, da se težave rešite s strojno opremo, kot da poskušate rešitve iskati s programsko opremo.

Nazadnje, če želite izvedeti več o tem, si lahko ogledate opombo v naslednja povezava.