Organizația RISC-V Foundation despre verificarea funcționării microkernel-ului pe sisteme cu arhitecturi de seturi de instrucțiuni RISC-V. Verificarea se reduce la a fiabilității funcționării seL4, care atestă conformitatea completă cu specificațiile definite într-un limbaj formal. Dovada fiabilității seL4 în sisteme critice bazate pe procesoare RISC-V RV64, care necesită un nivel ridicat de fiabilitate și garantarea absenței erorilor. Dezvoltatorii de software care rulează pe kernel-ul seL4 pot fi complet încrezători că, în cazul unei erori într-o parte a sistemului, acea eroare nu se va răspândi în restul sistemului și, în special, în părțile sale critice.
Inițial, microkernel-ul seL4 a fost verificat pentru procesoare ARM pe 32 de biți, iar ulterior pentru procesoare x86 pe 64 de biți. Se remarcă faptul că combinația între arhitectura hardware deschisă RISC-V și microkernel-ul deschis seL4 va permite atingerea unui nou nivel de securitate, deoarece componentele hardware ar putea fi de asemenea complet verificate în viitor, ceea ce nu este posibil pentru arhitecturile hardware proprietare.
În timpul verificării seL4 se presupune că echipamentul funcționează conform specificațiilor și că acestea descriu complet comportamentul sistemului, dar în realitate echipamentul nu este lipsit de erori, ceea ce este bine demonstrat de problemele recurente în mecanismul de execuție speculativă a instrucțiunilor. Platformele hardware deschise facilitează integrarea modificărilor legate de securitate – de exemplu, pentru blocarea tuturor canalelor posibile de scurgere prin canale externe, unde este mult mai eficient să rezolvi problema la nivel hardware decât să cauți soluții software.
Reamintim că arhitectura seL4 îndepărtarea părților pentru gestionarea resurselor nucleului în spațiul utilizatorului și aplicarea pentru astfel de resurse a acelorași instrumente de delimitare a accesului ca pentru resursele utilizatorului. Microkernelul nu oferă aberații de nivel înalt predefinite pentru gestionarea fișierelor, proceselor, conexiunilor de rețea etc., ci oferă doar mecanisme minime pentru gestionarea accesului la spațiul fizic de adresare, întreruperi și resursele procesorului. Abstracțiile de nivel înalt și driverele pentru interacțiunea cu hardware-ul sunt implementate separat deasupra microkernelului sub formă de sarcini executate la nivelul utilizatorului. Accesul acestor sarcini la resursele disponibile ale microkernelului este organizat prin definirea regulilor.
RISC-V oferă un sistem deschis și flexibil de instrucțiuni mașină, permițând crearea de microprocesoare pentru domenii de aplicație diverse, fără a necesita redevențe și fără a impune condiții de utilizare. RISC-V permite crearea de SoC-uri și procesoare complet deschise. În prezent, diverse companii și comunități dezvoltă, bazându-se pe specificația RISC-V, o serie de produse sub diverse licențe libere (BSD, MIT, Apache 2.0). câteva zeci de variante de nuclee de microprocesoare, SoC-uri și cipuri deja fabricate. Suportul pentru RISC-V este disponibil începând cu versiunile Glibc 2.27, binutils 2.30, gcc 7 și nucleul Linux 4.15.
Sursa: opennet.ro
