A fost finalizată verificarea formală matematică a fiabilității și securității funcționării microkernel-ului seL4 pe sistemele cu arhitectura setului de instrucțiuni AArch64. Verificarea se rezumă la o dovadă matematică a corectitudinii funcționării seL4, care dovedește conformitatea completă cu specificațiile definite în limbaj formal. Dovada fiabilității permite utilizarea seL4 în sisteme critice bazate pe procesoare ARM64, care necesită un nivel ridicat de securitate și garantează lipsa de erori.
Inițial, microkernel-ul seL4 a fost verificat pentru procesoare ARM pe 32 de biți, iar mai târziu pentru procesoare x86 și RISC-V pe 64 de biți. Verificarea garantează că, în cazul unei defecțiuni într-o parte a sistemului, această defecțiune nu se va extinde la restul sistemului și părțile sale critice. În contextul asigurării securității, verificarea confirmă că nucleul asigură un nivel adecvat de izolare a aplicațiilor, nu permite accesul acestora la informații fără autorizare și garantează că, în caz de compromitere a aplicațiilor secundare, atacul nu se va extinde la aplicațiile critice.
Arhitectura microkernel-ului seL4 este remarcabilă prin separarea părților pentru gestionarea resurselor nucleului în spațiul utilizatorului și aplicarea acelorași instrumente de delimitare a accesului pentru aceste resurse, ca pentru resursele utilizatorului. Microkernel-ul nu oferă abstractizări înalte pentru gestionarea fișierelor, proceselor, conexiunilor de rețea etc., ci oferă doar mecanisme Minime pentru gestionarea accesului la spațiul de adresare fizic, întreruperi și resurse ale procesorului. Abstractizările înalte și driverele pentru interacțiunea cu hardware-ul sunt implementate separat deasupra microkernel-ului sub formă de sarcini, care sunt executate la nivel de utilizator. Accesul acestor sarcini la resursele disponibile ale microkernel-ului se organizează prin definirea regulilor.
Sursa: opennet.ro
