A nyílt seL4 mikrokernelt fejlesztő projekt megkapta az ACM Software System Award díjat, amelyet az Association for Computing Machinery (ACM), a számítógépes rendszerek területén legtekintélyesebb nemzetközi szervezet évente ítél oda. A díjat a működési megbízhatóság matematikai bizonyítása terén elért eredményekért ítélik oda, amelyek igazolják a hivatalos nyelven meghatározott előírásoknak való teljes megfelelést, és elismerik a kritikus alkalmazásokban való felhasználásra való készséget. A seL4 projekt megmutatta, hogy az ipari operációs rendszer szintű tervek megbízhatóságának és biztonságának teljes formális ellenőrzése nem csak lehetséges, hanem a teljesítmény és a sokoldalúság veszélyeztetése nélkül is megvalósítható.
Az ACM Software System Award díját évente adják át az iparágra meghatározó hatást gyakorló szoftverrendszerek fejlesztésének elismerésére, új koncepciókat vezettek be vagy új kereskedelmi alkalmazási területeket nyitottak meg. A díj összege 35 ezer amerikai dollár. Az elmúlt években az ACM-díjat a GCC és az LLVM projektek, valamint alapítóik Richard Stallman és Chris Latner kapták. A díj olyan projekteket és technológiákat is elismert, mint a UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB és Eclipse .
A seL4 mikrokernel architektúra figyelemre méltó arról, hogy a kernel erőforrások kezeléséhez szükséges alkatrészeket a felhasználói térbe mozgatja, és ugyanazokat a hozzáférés-vezérlő eszközöket használja az erőforrásokhoz, mint a felhasználói erőforrásokhoz. A mikrokernel nem ad kész magas szintű absztrakciókat a fájlok, folyamatok, hálózati kapcsolatok és hasonlók kezelésére, ehelyett csak minimális mechanizmusokat biztosít a fizikai címtérhez, a megszakításokhoz és a processzorerőforrásokhoz való hozzáférés szabályozására. A magas szintű absztrakciók és a hardverrel való interakcióhoz szükséges illesztőprogramok külön vannak implementálva a mikrokernel tetején, felhasználói szintű feladatok formájában. Az ilyen feladatoknak a mikrokernel rendelkezésére álló erőforrásokhoz való hozzáférése szabályok meghatározásán keresztül történik.
Forrás: opennet.ru