Fundația RISC-V a anunțat că a verificat cum funcționează microkernelul seL4 în sistemele cu arhitectura setului de instrucțiuni RISC-V. În care procesul de verificare este redus la dovada matematică a fiabilității seL4, ceea ce indică respectarea deplină a specificațiilor specificate într-un limbaj formal.
Testarea fiabilității permite utilizarea seL4 în sistemele critice de misiune bazate pe procesoare RISC-V RV64, care necesită un nivel mai ridicat de fiabilitate și nu garantează eșecul.
Dezvoltatorii de software care rulează deasupra nucleului seL4 pot fi complet încrezători că, în cazul unei defecțiuni într-o parte a sistemului, această defecțiune nu se va răspândi în restul sistemului și, în special, în părțile sale critice.
Despre seL4
Arhitectura seL4 se remarcă prin eliminarea părților pentru a gestiona resursele nucleului în spațiul utilizatorului și utilizați aceleași metode de control al accesului pentru astfel de resurse ca și pentru resursele utilizatorilor.
Microcernelul nu oferă abstracții la nivel înalt deja pregătit să gestioneze fișiere, procese, conexiuni de rețea etc., dar în schimb oferă doar mecanisme minime pentru a controla accesul la spațiul de adrese fizic, întrerupe și resurse procesor.
Abstracții la nivel înalt și controlere pentru interacțiunea cu computerul sunt implementate separat pe microkernel sub formă de sarcini efectuate la nivel de utilizator.
Accesul unor astfel de sarcini la resursele disponibile în microkernel este organizat prin definirea regulilor.
RISC-V oferă un sistem deschis și flexibil a instrucțiunilor mașinii care permite crearea de microprocesoare pentru aplicații arbitrare, fără a necesita deduceri și fără a impune condiții de utilizare.
RISC-V vă permite să creați SoC-uri și procesoare complet deschise. În prezent, pe baza specificației RISC-V, mai multe companii și comunități sub diferite licențe gratuite (BSD, MIT, Apache 2.0) dezvoltă câteva zeci de variante de nuclee de microprocesor deja produse, SoC-uri și cipuri.
Suportul RISC-V a existat de la lansarea Glibc 2.27, binutils 2.30, gcc 7 și kernel-ul Linux 4.15.
Despre testarea microcernelului seL4
Inițial, microkernelul seL4 a fost verificat pentru procesoarele ARM pe 32 de biți, Și mai târziu pentru procesoarele x86 pe 64 de biți.
Se observă că combinația dintre arhitectura hardware deschisă RISC-V și microkernelul deschis seL4 va atinge un nou nivel de securitate, deoarece componentele hardware viitoare pot fi, de asemenea, verificate pe deplin, ceea ce este imposibil de realizat pentru arhitecturile hardware proprietare.
Când verificăm seL4, trebuie să presupunem că hardware-ul funcționează corect (adică, așa cum se specifică). Aceasta presupune că există o specificație fără echivoc în primul rând, ceea ce nu este cazul tuturor hardware-urilor.
Dar chiar și atunci când o astfel de specificație există și este formală (adică este scrisă într-un formalism matematic care susține raționamentul matematic despre proprietățile sale), de unde știm că captează de fapt comportamentul hardware-ului?
Realitatea este că putem fi destul de siguri că nu este. Hardware-ul nu diferă de software, deoarece ambele sunt buggy.
Dar a avea un ISA deschis are avantaje care merg dincolo de a fi fără drepturi de autor. Unul este că permite implementări hardware open source.
La verificarea seL4, se presupune că echipamentul funcționează așa cum este indicat și caietul de sarcini descrie pe deplin comportamentul sistemului, dar de fapt echipamentul nu are erori, ceea ce este bine demonstrat de problemele care apar în mod regulat în instrucțiunile mecanismului de execuție speculativă.
Platformele hardware deschise simplifică integrarea modificărilor legat de securitate, de exemplu, pentru a bloca toate canalele de scurgere posibile prin canale terțe, unde este mult mai eficient să scapi de o problemă prin hardware decât să încerci să găsești soluții prin software.
În cele din urmă, dacă doriți să aflați mai multe despre aceasta, puteți consulta nota în următorul link.
Pentru mine, acest procesor este ceva care mă cheamă foarte mult. Rămâne doar pentru un câine de grăsime să facă un computer pe care îl putem cumpăra.
Problema ARM este ceva care mă scârțâie, ai văzut deja ce s-a întâmplat cu Huawei cu sancțiunile. Sunt clar că pentru RISC-V este o soluție mult mai bună la toate nivelurile. În acest moment Huawei a pus deja ochii pe el și poate că în viitor vor avea echipamente cu acest micro. Dacă da, cu siguranță vor fi mai multe companii care îl vor adopta și pentru mine ar fi idealul și mai presus de toate că distribuțiile îl susțin și nu doar ARM așa cum se întâmplă cu majoritatea.
+10