RISC-V je provjerio mikrojezru seL4 na svojim RV64 procesorima

Zaklada RISC-V objavila je da je provjerila kako mikrojezgro djeluje seL4 u sustavima s arhitektura skupa uputa RISC-V. U kojem se postupak provjere svodi na matematički test pouzdanosti seL4, što ukazuje na potpunu usklađenost sa specifikacijama navedenim u službenom jeziku.

Ispitivanje pouzdanosti omogućuje upotrebu seL4 u kritičnim sustavima koji se temelje na RISC-V procesorima RV64, što zahtijeva višu razinu pouzdanosti i ne jamči neuspjeh.

Programeri softvera koji rade na jezgru seL4 mogu biti potpuno sigurni da se u slučaju kvara na jednom dijelu sustava taj kvar neće proširiti na ostatak sustava, a posebno na njegove kritične dijelove.

O seL4

Arhitektura seL4 je značajan po uklanjanju dijelova za upravljanje resursima jezgre u korisničkom prostoru i koristiti iste metode kontrole pristupa za takve resurse kao i za korisničke resurse.

Mikro zrno ne pruža apstrakcije na visokoj razini već pripremljen za upravljanje datotekama, procesima, mrežnim vezama itd., ali umjesto toga pruža samo minimalne mehanizme za kontrolu pristupa fizičkom adresnom prostoru, prekidi i resursi procesora.

Apstrakcije na visokoj razini i kontroleri za interakciju s računalom implementirani su odvojeno na vrh mikrokera u obliku zadataka izvršenih na korisničkoj razini.

Pristup takvih zadataka resursima koji su dostupni u mikro jezgri organiziran je kroz definiranje pravila.

RISC-V pruža otvoren i fleksibilan sustav strojnih uputa koje omogućuje stvaranje mikroprocesora za proizvoljne primjene, bez potrebe za odbitcima i bez nametanja uvjeta korištenja.

RISC-V omogućuje vam stvaranje potpuno otvorenih procesora i SoC-ova. Trenutno, na temelju specifikacije RISC-V, razne tvrtke i zajednice pod raznim besplatnim licencama (BSD, MIT, Apache 2.0) razvijaju nekoliko desetaka inačica već proizvedenih mikroprocesorskih jezgri, SoC-ova i čipova.

Podrška za RISC-V postoji od izdavanja Glibc 2.27, binutils 2.30, gcc 7 i Linux 4.15 kernela.

O testiranju mikrojezri seL4

U početku, mikro jezgra seL4 je provjeren za 32-bitne ARM procesore, I kasnije za x86 64-bitne procesore.

Primjećuje se da kombinacija otvorene hardverske arhitekture RISC-V s otvorenim mikrojezrom seL4 će postići novu razinu sigurnostijer se hardverske komponente u budućnosti također mogu u potpunosti provjeriti, što je nemoguće postići za vlasničke hardverske arhitekture.

Kada provjeravamo seL4, moramo pretpostaviti da hardver ispravno radi (to jest, kako je navedeno). To pretpostavlja da u prvom redu postoji jednoznačna specifikacija, što nije slučaj za sav hardver. 

Ali čak i kada takva specifikacija postoji, a ona je formalna (to jest, pretvorena u matematički formalizam koji podržava matematičko rasuđivanje o njezinim svojstvima), kako znamo da zapravo bilježi ponašanje hardvera? 

Stvarnost je takva da možemo biti prilično sigurni da nije. Hardver se ne razlikuje od softvera po tome što su obje programske pogreške.

Imati otvoreni ISA ima prednosti koje nadilaze mogućnost besplatnog korištenja. Jedan je taj što omogućuje implementaciju hardvera otvorenog koda.

Prilikom provjere seL4, pretpostavlja se da oprema radi kako je naznačeno i specifikacija u potpunosti opisuje ponašanje sustava, ali zapravo oprema ne sadrži pogreške, što dobro pokazuju problemi koji se redovito pojavljuju u uputama mehanizma spekulativnog izvršenja.

Otvorene hardverske platforme pojednostavljuju integraciju promjena povezane sa sigurnošću, na primjer, za blokiranje svih mogućih kanala curenja putem nezavisnih kanala, gdje je mnogo učinkovitije riješiti se hardverskim problemom nego pokušati pronaći rješenja softverskim putem.

Napokon, ako želite znati više o tome, možete pogledati bilješku u sljedeći link.