Proiectul care dezvoltă microkernelul deschis seL4 a primit premiul ACM Software System Award, acordat anual de Asociația pentru Calcul (ACM), cea mai autoritară organizație internațională în domeniul sistemelor informatice. Premiul a fost acordat pentru realizările în domeniul demonstrației matematice a fiabilității operării, care dovedește conformitatea completă cu specificațiile definite în limbaj formal și recunoaște pregătirea pentru utilizarea în aplicații critice. Proiectul seL4 a demonstrat că este posibil să se efectueze o verificare formală completă a fiabilității și securității pentru proiecte la nivelul sistemelor de operare industriale, fără a compromite performanța și versatilitatea.
Premiul ACM Software System Award este înmânat anual pentru dezvoltarea sistemelor software care au avut un impact definitoriu asupra industriei, introducând concepte noi sau descoperind noi domenii de aplicare comercială. Valoarea premiului este de 35 de mii de dolari SUA. În anii anteriori, premiile ACM au fost acordate proiectelor GCC și LLVM, precum și fondatorilor lor Richard Stallman și Chris Lattner. De asemenea, au fost recunoscute proiecte și tehnologii precum UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB și Eclipse.
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
