Fundația RISC-V despre verificarea funcționării microkernel-ului pe sisteme cu arhitectură set de instrucțiuni RISC-V. Verificarea se reduce la fiabilitatea funcționării seL4, care indică conformitatea deplină cu specificațiile specificate în limbajul formal. Dovada de fiabilitate seL4 în sisteme critice bazate pe procesoare RISC-V RV64 care necesită un nivel crescut de fiabilitate și garantează absența defecțiunilor. Dezvoltatorii de software care rulează pe partea superioară a nucleului seL4 pot fi complet încrezători că, dacă există o defecțiune într-o parte a sistemului, această defecțiune nu se va răspândi la restul sistemului și, în special, la părțile sale critice.
Microkernel-ul seL4 a fost verificat inițial pentru procesoarele ARM pe 32 de biți, iar mai târziu pentru procesoarele x64 pe 86 de biți. Se remarcă faptul că combinația dintre arhitectura hardware deschisă RISC-V cu microkernel-ul deschis seL4 va atinge un nou nivel de securitate, deoarece componentele hardware pot fi, de asemenea, verificate pe deplin în viitor, ceea ce este imposibil de realizat pentru arhitecturile hardware proprietare.
La verificarea seL4, se presupune că echipamentul funcționează așa cum este menționat și ca specificația descrie pe deplin comportamentul sistemului, dar în realitate echipamentul nu este lipsit de erori, ceea ce este demonstrat în mod clar de problemele care apar în mod regulat în mecanismul de execuție speculativă a instrucțiuni. Platformele hardware deschise facilitează integrarea modificărilor legate de securitate - de exemplu, pentru a bloca toate scurgerile posibile de canal lateral, unde este mult mai eficient să scapi de problema din hardware decât să încerci să găsești soluții în software.
Amintiți-vă că arhitectura seL4 mutarea părților pentru gestionarea resurselor nucleului în spațiul utilizatorului și aplicarea acelorași mijloace de control al accesului pentru astfel de resurse ca și pentru resursele utilizatorului. Microkernel-ul nu oferă abstracții gata făcute la nivel înalt pentru gestionarea fișierelor, proceselor, conexiunilor de rețea și altele asemenea; în schimb, oferă doar mecanisme minime pentru controlul accesului la spațiul de adrese fizice, întreruperi și resurse de procesor. Abstracțiile de nivel înalt și driverele pentru interacțiunea cu hardware-ul sunt implementate separat deasupra microkernel-ului sub formă de sarcini la nivel de utilizator. Accesul unor astfel de sarcini la resursele disponibile microkernel-ului este organizat prin definirea regulilor.
RISC-V oferă un sistem de instruire a mașinii deschis și flexibil, care permite construirea de microprocesoare pentru aplicații arbitrare fără a necesita drepturi de autor sau șiruri atașate pentru utilizare. RISC-V vă permite să creați SoC-uri și procesoare complet deschise. În prezent, bazat pe specificația RISC-V de către diferite companii și comunități sub diferite licențe gratuite (BSD, MIT, Apache 2.0) Câteva zeci de variante de nuclee de microprocesoare, SoC-uri și cipuri sunt deja în producție. Suportul pentru RISC-V este prezent încă de la lansările Glibc 2.27, binutils 2.30, gcc 7 și kernel. Linux 4.15.
Sursa: opennet.ru
