Projekt, ki razvija odprto mikrojedro seL4, je prejel nagrado ACM Software System Award, ki jo letno podeljuje Asociacija računalniške tehnike (ACM), najuglednejša mednarodna organizacija na področju računalniških sistemov. Nagrada je bila podeljena za dosežke na področju matematičnega dokazovanja zanesljivosti delovanja, ki dokazuje popolno skladnost s specifikacijami v formalnem jeziku in priznava pripravljenost za uporabo v kritičnih aplikacijah. Projekt seL4 je pokazal, da je mogoče ne le popolnoma izvesti formalno verifikacijo zanesljivosti in varnosti za projekte industrijskih operacijskih sistemov, temveč to doseči brez kompromisov pri zmogljivosti in univerzalnosti.
Nagrada ACM Software System Award se letno podeljuje za razvoj programski sistemov, ki so pomembno vplivali na panogo, uvedli nove koncepte ali razkrili nove področja komercialne uporabe. Vrednost nagrade znaša 35 tisoč dolarjev ZDA. Pretekla leta so nagrade ACM prejele projekte GCC in LLVM, ter njuna ustanovitelja Richard Stallman in Chris Lattner. Nagrada je tudi prepoznala projekte in tehnologije, kot 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 se odlikuje po tem, da delčke za upravljanje virov jedra prenaša v uporabniški prostor in uporablja za te vire iste metode za nadzor dostopa, kot za uporabniške vire. Mikrojedro ne ponuja pripravljene visoko nivojske abstrakcije za upravljanje datotek, procesov, omrežnih povezav itd., temveč zagotavlja le minimalne mehanizme za upravljanje dostopa do fizičnega naslovnega prostora, prekinitev in virov procesorja. Visoko nivojske abstrakcije in gonilniki za interakcijo s strojno opremo se izvajajo ločeno nad mikrojedrom v obliki nalog, ki se izvajajo na uporabniški ravni. Dostop teh nalog do virov mikrojedra je organiziran z določanjem pravil.
Izvor: opennet.ru
