Projekt vyvíjející otevřené mikrojádro seL4 získal cenu ACM Software System Award, kterou každoročně uděluje Association for Computing Machinery (ACM), nejuznávanější mezinárodní organizace v oblasti počítačových systémů. Cena se uděluje za úspěchy v oblasti matematického důkazu spolehlivosti provozu, který prokazuje plnou shodu se specifikacemi uvedenými ve formálním jazyce a uznává připravenost k použití v kritických aplikacích. Projekt seL4 ukázal, že u návrhů na úrovni průmyslových operačních systémů je nejen možné plně formálně ověřit spolehlivost a bezpečnost, ale také toho dosáhnout bez kompromisů ve výkonu a všestrannosti.
Ocenění ACM Software System Award se uděluje každoročně jako ocenění vývoje softwarových systémů, které mají definitivní dopad na průmysl, zavádějí nové koncepty nebo otevírají nové oblasti komerčních aplikací. Výše ocenění je 35 tisíc amerických dolarů. V minulých letech byly ceny ACM uděleny projektům GCC a LLVM a jejich zakladatelům Richardu Stallmanovi a Chrisi Latnerovi. Ocenění také ocenilo projekty a technologie jako UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB a Eclipse .
Architektura mikrojádra seL4 se vyznačuje přesouváním částí pro správu zdrojů jádra do uživatelského prostoru a používáním stejných nástrojů pro řízení přístupu k takovým zdrojům jako k uživatelským zdrojům. Mikrokernel neposkytuje hotové abstrakce na vysoké úrovni pro správu souborů, procesů, síťových připojení a podobně, místo toho poskytuje pouze minimální mechanismy pro řízení přístupu k fyzickému adresnímu prostoru, přerušením a zdrojům procesoru. Vysokoúrovňové abstrakce a ovladače pro interakci s hardwarem jsou implementovány odděleně nad mikrokernelem ve formě úloh na uživatelské úrovni. Přístup těchto úkolů ke zdrojům, které má mikrojádro k dispozici, je organizován prostřednictvím definice pravidel.
Zdroj: opennet.ru