Fundacija RISC-V o preverjanju delovanja mikrojedra na sistemih z arhitekturo nabora ukazov RISC-V. Preverjanje se zmanjša na zanesljivost delovanja seL4, kar kaže na popolno skladnost s specifikacijami, določenimi v formalnem jeziku. Dokazilo o zanesljivosti seL4 v kritičnih sistemih na osnovi procesorjev RISC-V RV64, ki zahtevajo povečano stopnjo zanesljivosti in zagotavljajo odsotnost okvar. Razvijalci programske opreme, ki se izvaja na vrhu jedra seL4, so lahko popolnoma prepričani, da če pride do okvare v enem delu sistema, se ta okvara ne bo razširila na preostanek sistema in še posebej na njegove kritične dele.
Mikrojedro seL4 je bilo sprva preverjeno za 32-bitne procesorje ARM, kasneje pa za 64-bitne procesorje x86. Opozoriti je treba, da bo kombinacija odprte arhitekture strojne opreme RISC-V z odprtim mikrojedrom seL4 dosegla novo raven varnosti, saj bo mogoče komponente strojne opreme tudi v prihodnosti v celoti preveriti, kar je nemogoče doseči pri lastniških arhitekturah strojne opreme.
Pri preverjanju seL4 se predpostavlja, da oprema deluje kot je navedeno in specifikacija v celoti opisuje obnašanje sistema, v resnici pa oprema ni brez napak, kar jasno dokazujejo redno pojavljajoče se težave v mehanizmu špekulativnega izvajanja navodila. Odprte platforme strojne opreme olajšajo integracijo sprememb, povezanih z varnostjo – na primer blokiranje vseh možnih stranskih uhajanj, kjer je veliko učinkoviteje znebiti se težave v strojni opremi, kot pa poskušati najti rešitve v programski opremi.
Spomnimo se, da je arhitektura seL4 premikanje delov za upravljanje virov jedra v uporabniški prostor in uporaba istih sredstev za nadzor dostopa za take vire kot za uporabniške vire. Mikrojedro ne zagotavlja pripravljenih visokonivojskih abstrakcij za upravljanje datotek, procesov, omrežnih povezav in podobnega, temveč le minimalne mehanizme za nadzor dostopa do fizičnega naslovnega prostora, prekinitev in virov procesorja. Visokonivojske abstrakcije in gonilniki za interakcijo s strojno opremo so implementirani ločeno na vrhu mikrojedra v obliki nalog na ravni uporabnika. Dostop takšnih nalog do virov, ki so na voljo mikrojedru, je organiziran z definicijo pravil.
RISC-V zagotavlja odprt in prilagodljiv sistem strojnih ukazov, ki omogoča izdelavo mikroprocesorjev za poljubne aplikacije, ne da bi za uporabo zahtevali licenčnine ali nize. RISC-V vam omogoča ustvarjanje popolnoma odprtih SoC-jev in procesorjev. Trenutno temelji na specifikaciji RISC-V različnih podjetij in skupnosti pod različnimi brezplačnimi licencami (BSD, MIT, Apache 2.0) več deset variant mikroprocesorskih jeder, SoC-jev in že izdelanih čipov. Podpora za RISC-V je prisotna od izdaj Glibc 2.27, binutils 2.30, gcc 7 in jedra Linuxa 4.15.
Vir: opennet.ru