Projekt otvorene mikrojezgre seL4 dobio je nagradu ACM Software System Award, godišnju nagradu koju dodjeljuje Association for Computing Machinery (ACM), najuglednija međunarodna organizacija u području računalnih sustava. Nagrada se dodjeljuje za postignuća u području matematičkog dokaza rada, koji ukazuje na potpunu usklađenost sa specifikacijama danim u formalnom jeziku i prepoznaje spremnost za korištenje u kritičnim aplikacijama. Projekt seL4 pokazao je da nije samo moguće u potpunosti formalno provjeriti pouzdanost i sigurnost za projekte na razini industrijskih operativnih sustava, već i postići to bez žrtvovanja performansi i svestranosti.
ACM Software System Award dodjeljuje se svake godine kako bi se prepoznao razvoj softverskih sustava koji su imali odlučujući utjecaj na industriju, uvodeći nove koncepte ili otvarajući nove komercijalne aplikacije. Iznos nagrade je 35 tisuća američkih dolara. Proteklih godina ACM nagrade dodijeljene su projektima GCC i LLVM, te njihovim osnivačima Richardu Stallmanu i Chrisu Latneru. Ostali projekti i tehnologije koji su također nagrađeni 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 mikrojezgre seL4 značajna je po uklanjanju dijelova za upravljanje resursima jezgre u korisničkom prostoru i po primjeni istih načina kontrole pristupa za takve resurse kao i za korisničke resurse. Mikrokernel ne pruža gotove apstrakcije visoke razine za upravljanje datotekama, procesima, mrežnim vezama i slično, umjesto toga pruža samo minimalne mehanizme za kontrolu pristupa fizičkom adresnom prostoru, prekidima i resursima procesora. Apstrakcije visoke razine i upravljački programi za interakciju s hardverom implementirani su zasebno na vrhu mikrojezgre u obliku zadataka na razini korisnika. Pristup takvih zadataka resursima dostupnim mikrojezgri organiziran je kroz definiranje pravila.
Izvor: opennet.ru