Projekat razvoja otvorenog mikrokernela seL4 dobio je nagradu ACM Software System Award koju svake godine dodeljuje Asocijacija za računarske mašine (ACM), najautoritativnija međunarodna organizacija u oblasti računarskih sistema. Nagrada se dodeljuje za dostignuća u oblasti matematičkog dokaza pouzdanosti rada, koji pokazuje punu usklađenost sa specifikacijama navedenim na formalnom jeziku i priznaje spremnost za upotrebu u kritičnim aplikacijama. Projekat seL4 je pokazao da nije moguće samo u potpunosti formalno potvrditi pouzdanost i sigurnost za dizajn na nivou industrijskog operativnog sistema, već i to postići bez žrtvovanja performansi ili svestranosti.
ACM Software System Award dodjeljuje se svake godine kako bi se odao priznanje razvoju softverskih sistema koji su imali odlučujući utjecaj na industriju, uvodeći nove koncepte ili otvarajući nova područja komercijalne primjene. Iznos nagrade je 35 hiljada američkih dolara. Proteklih godina ACM nagrade dodijeljene su projektima GCC i LLVM, te njihovim osnivačima Richardu Stallmanu i Chrisu Latneru. Nagrada je takođe prepoznala projekte i tehnologije kao što su UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB i Eclipse .
Arhitektura seL4 mikrokernela je istaknuta po pokretnim dijelovima za upravljanje resursima kernela u korisnički prostor i korištenju istih alata za kontrolu pristupa za takve resurse kao i za korisničke resurse. Mikrokernel ne pruža gotove apstrakcije visokog nivoa za upravljanje datotekama, procesima, mrežnim vezama i slično, već samo minimalne mehanizme za kontrolu pristupa fizičkom adresnom prostoru, prekidima i procesorskim resursima. Apstrakcije visokog nivoa i drajveri za interakciju sa hardverom implementirani su odvojeno na vrhu mikrokernela u obliku zadataka na nivou korisnika. Pristup takvih zadataka resursima dostupnim mikrokernelu je organizovan kroz definiciju pravila.
izvor: opennet.ru
