SeL4 opna örkjarnaverkefnið hefur hlotið ACM Software System Award, árleg verðlaun sem veitt eru af Association for Computing Machinery (ACM), virtustu alþjóðasamtökunum á sviði tölvukerfa. Verðlaunin eru veitt fyrir árangur á sviði stærðfræðilegrar sönnunar á rekstri, sem gefur til kynna að fullu samræmi við forskriftir sem gefnar eru á formlegu tungumáli og viðurkennir reiðubúinn til notkunar í mikilvægum forritum. SeL4 verkefnið hefur sýnt að það er ekki aðeins hægt að sannreyna að fullu formlega áreiðanleika og öryggi fyrir verkefni á sviði iðnaðarstýrikerfa, heldur einnig að ná þessu án þess að fórna frammistöðu og fjölhæfni.
ACM hugbúnaðarkerfisverðlaunin eru veitt árlega til að viðurkenna þróun hugbúnaðarkerfa sem hafa haft afgerandi áhrif á iðnaðinn, kynning á nýjum hugmyndum eða opnun ný viðskiptaforrit. Upphæð verðlaunanna er 35 þúsund Bandaríkjadalir. Undanfarin ár hafa ACM verðlaun verið veitt GCC og LLVM verkefnunum og stofnendum þeirra Richard Stallman og Chris Latner. Önnur verkefni og tækni sem einnig voru verðlaunuð voru UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB og eclipse .
Arkitektúr örkjarna seL4 er áberandi fyrir að fjarlægja hluta til að stjórna kjarnaauðlindum í notendarými og fyrir að beita sömu aðgangsstýringum fyrir slík auðlind og fyrir notendaauðlindir. Örkjarnan veitir ekki út-af-the-box útdrætti á háu stigi til að stjórna skrám, ferlum, nettengingum og þess háttar, í staðinn veitir hann aðeins lágmarksaðferðir til að stjórna aðgangi að líkamlegu heimilisfangarýminu, truflunum og örgjörvaauðlindum. Útdrættir á háu stigi og rekla fyrir samskipti við vélbúnað eru útfærð sérstaklega ofan á örkjarnanum í formi verkefna á notendastigi. Aðgangur slíkra verkefna að þeim auðlindum sem örkjarnan hefur tiltækt er skipulagður með skilgreiningu reglna.
Heimild: opennet.ru