Projekt odprtega mikrojedra seL4 je prejel nagrado ACM Software System Award, letno nagrado, ki jo podeljuje Association for Computing Machinery (ACM), najuglednejša mednarodna organizacija na področju računalniških sistemov. Nagrada se podeljuje za dosežke na področju matematičnega dokaza delovanja, ki kaže popolno skladnost s specifikacijami, podanimi v formalnem jeziku, in priznava pripravljenost za uporabo v kritičnih aplikacijah. Projekt seL4 je pokazal, da ni mogoče le v celoti formalno preveriti zanesljivosti in varnosti za projekte na ravni industrijskih operacijskih sistemov, ampak to tudi doseči brez žrtvovanja zmogljivosti in vsestranskosti.
Nagrada ACM Software System Award se podeljuje vsako leto kot priznanje za razvoj programskih sistemov, ki so odločilno vplivali na industrijo z uvajanjem novih konceptov ali odpiranjem novih komercialnih aplikacij. Znesek nagrade je 35 tisoč ameriških dolarjev. V preteklih letih so nagrade ACM prejeli projekti GCC in LLVM ter njuna ustanovitelja Richard Stallman in Chris Latner. Drugi projekti in tehnologije, ki so bili prav tako nagrajeni, so UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB in eclipse .
Arhitektura mikrojedra seL4 je znana po odstranitvi delov za upravljanje virov jedra v uporabniškem prostoru in po uporabi istih načinov nadzora dostopa za take vire kot za uporabniške vire. Mikrojedro ne zagotavlja takoj pripravljenih visokonivojskih abstrakcij za upravljanje datotek, procesov, omrežnih povezav in podobnega, namesto tega ponuja le minimalne mehanizme za nadzor dostopa do fizičnega naslovnega prostora, prekinitev in virov procesorja. Visokonivojske abstrakcije in gonilniki za interakcijo s strojno opremo so implementirani ločeno na vrhu mikrojedra v obliki nalog na ravni uporabnika. Dostop takih nalog do virov, ki so na voljo mikrojedru, je organiziran z definicijo pravil.
Vir: opennet.ru