RISC-V je verificirao mikrojezgre seL4 na svojim RV64 procesorima

Fondacija RISC-V objavila je da je verifikovala rad mikrokernela seL4 u sistemima sa arhitektura skupa instrukcija RISC-V. U kojem se proces verifikacije svodi na matematički dokaz pouzdanosti seL4, što ukazuje na potpunu usklađenost sa specifikacijama navedenim u formalnom jeziku.

Test pouzdanosti omogućava da se seL4 koristi u kritičnim sistemima baziranim na RISC-V procesorima RV64, što zahtijeva viši nivo pouzdanosti i ne garantuje kvar.

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

O seL4

Arhitektura seL4 je prepoznatljiv po uklanjanju dijelova za upravljanje resursima kernela u korisničkom prostoru i koristiti iste metode kontrole pristupa za takve resurse kao i za resurse korisnika.

Mikrokernel ne pruža apstrakcije na visokom nivou već spreman za upravljanje datotekama, procesima, mrežnim vezama, itd., već radije pruža samo minimalne mehanizme za kontrolu pristupa fizičkom adresnom prostoru, prekide i procesorske resurse.

Apstrakcije visokog nivoa i drajveri za interakciju sa računarom implementirani su odvojeno na vrhu mikrokernela u obliku zadataka koji se obavljaju na nivou korisnika.

Pristup takvih zadataka resursima dostupnim u mikrokernelu je organizovan kroz definiciju pravila.

RISC-V pruža otvoren i fleksibilan sistem mašinskih instrukcija koje omogućava kreiranje mikroprocesora za proizvoljne aplikacije, bez potrebe za odbicima i bez nametanja uslova korišćenja.

RISC-V vam omogućava da kreirate potpuno otvorene SoC-ove i procesore. Trenutno, na osnovu RISC-V specifikacije, nekoliko kompanija i zajednica pod raznim besplatnim licencama (BSD, MIT, Apache 2.0) razvija nekoliko desetina varijanti već proizvedenih mikroprocesorskih jezgara, SoC-a i čipova.

RISC-V podrška je prisutna od izdanja Glibc 2.27, binutils 2.30, gcc 7 i Linux 4.15 kernela.

O seL4 testovima mikrokernela

U početku, mikrokernel seL4 je verifikovan za 32-bitne ARM procesore, y kasnije za 86-bitne x64 procesore.

Primećeno je da je kombinacija RISC-V otvorene hardverske arhitekture sa otvorenim mikrojezgrom seL4 će postići novi nivo sigurnosti, budući da se hardverske komponente u budućnosti takođe mogu u potpunosti verificirati, što je nemoguće postići za vlasničke hardverske arhitekture.

Kada provjeravamo seL4, moramo pretpostaviti da hardver radi ispravno (tj. kako je navedeno). To pretpostavlja da prije svega postoji nedvosmislena specifikacija, što nije slučaj za sav hardver. 

Ali čak i kada takva specifikacija postoji, i formalna je (tj. zasnovana na matematičkom formalizmu koji podržava matematičko rezonovanje o svojim svojstvima), kako možemo znati da stvarno bilježi ponašanje hardvera? 

Realnost je da možemo biti prilično sigurni da to nije slučaj. Hardver se ne razlikuje od softvera po tome što oba imaju greške.

Ali otvaranje ISA-e ima prednosti koje nadilaze mogućnost besplatnog plaćanja naknade. Jedna je da vam omogućava da imate hardverske implementacije otvorenog koda.

Prilikom provjere seL4 pretpostavlja se da oprema radi kako je navedeno i specifikacija u potpunosti opisuje ponašanje sistema, ali u stvari oprema nije bez grešaka, što dobro pokazuju problemi koji se redovno javljaju u mehanizmu spekulativnog izvršenja Uputstva .

Otvorene hardverske platforme pojednostavljuju integraciju promjena vezano za sigurnost, na primjer, blokirati sve moguće kanale curenja putem kanala trećih strana, gdje je mnogo efikasnije riješiti se problema putem hardvera nego pokušati pronaći rješenja putem softvera.

Konačno, ako želite saznati više o tome, možete pogledati napomenu u sljedeći link.