Organizacija RISC-V Foundation o verifikaciji rada mikrojezgre na sustavima s arhitekturom skupa instrukcija RISC-V. Verifikacija se svodi na pouzdanosti rada seL4, što ukazuje na potpuno usklađivanje s unaprijed definiranim formalnim specifikacijama. Dokazivanje pouzdanosti seL4 u kritičnim sustavima temeljenim na RISC-V RV64 procesorima, koji zahtijevaju povećanu razinu pouzdanosti i garantiraju odsutnost grešaka. Programeri softvera koji radi na seL4 jezgru mogu biti potpuno sigurni da u slučaju kvara u jednom dijelu sustava, taj kvar neće utjecati na ostatak sustava, posebno na njegove kritične dijelove.
U početku je mikrojezgra seL4 verifikovana za 32-bitne ARM procesore, a kasnije za 64-bitne x86 procesore. Ističe se da kombinacija otvorene hardverske arhitekture RISC-V s otvorenim mikrojezgro seL4 omogućava postizanje novog nivoa sigurnosti, jer hardverske komponente u budućnosti također mogu biti potpuno verifikovane, što nije moguće postići s vlasničkim hardverskim arhitekturama.
Prilikom verifikacije seL4 pretpostavlja se da oprema radi kako je navedeno i da specifikacija potpuno opisuje ponašanje sustava, ali u stvarnosti oprema nije oslobođena grešaka, što se dobro pokazuje redovnim problemima u mehanizmu spekulativnog izvršavanja instrukcija. Otvorene hardverske platforme olakšavaju integraciju promjena povezanih s sigurnošću - na primjer, za blokiranje svih mogućih kanala curenja putem bočnih kanala, gdje je često učinkovitije riješiti problem hardverski nego tražiti zaobilaženja softverski.
Podsjetimo da je arhitektura seL4 izdvajanjem dijelova za upravljanje resursima jezgre u prostor korisnika i primjenom istih sredstava kontrole pristupa za te resurse kao i za korisničke resurse. Mikrojezgore ne pruža gotove visokorazinske apstrakcije za upravljanje datotekama, procesima, mrežnim vezama itd., umjesto toga, ona pruža samo minimalne mehanizme za upravljanje pristupom fizičkom adresnom prostoru, prekidima i procesorskim resursima. Visoko-razinske apstrakcije i upravljački programi za interakciju s hardverom realiziraju se odvojeno preko mikrojezgre u obliku zadataka koji se izvode na korisničkoj razini. Pristup takvih zadataka resursima koje mikrojezgore pruža organizira se kroz definiranje pravila.
RISC-V omogućava otvoreni i fleksibilni sustav mašinskih instrukcija, koji omogućuje stvaranje mikroprocesora za razne primjene bez zahtjeva za licencama i bez uvjeta za korištenje. RISC-V omogućava stvaranje potpuno otvorenih SoC-ova i procesora. Trenutno su na temelju specifikacije RISC-V različite tvrtke i zajednice razvijaju razne slobodne licence (BSD, MIT, Apache 2.0). nekoliko desetaka varijanti jezgra mikroprocesora, SoC-ova i već proizvedenih čipova. Podrška za RISC-V je prisutna od izdanja Glibc 2.27, binutils 2.30, gcc 7 i jezgre Linux 4.15.
Izvor: opennet.ru
