Projekti i hapur i mikrokernelit seL4 ka marrë çmimin ACM Software System Award, një çmim vjetor i dhënë nga Shoqata për Makineri Kompjuterike (ACM), organizata më e respektuar ndërkombëtare në fushën e sistemeve kompjuterike. Çmimi jepet për arritjet në fushën e provës matematikore të funksionimit, e cila tregon përputhshmëri të plotë me specifikimet e dhëna në një gjuhë zyrtare dhe njeh gatishmërinë për përdorim në aplikacionet kritike të misionit. Projekti seL4 ka treguar se jo vetëm që është e mundur të verifikohet plotësisht zyrtarisht besueshmëria dhe siguria për projektet në nivelin e sistemeve operative industriale, por edhe të arrihet kjo pa sakrifikuar performancën dhe shkathtësinë.
Çmimi i Sistemit të Softuerit ACM prezantohet çdo vit për të njohur zhvillimin e sistemeve softuerike që kanë pasur një ndikim përcaktues në industri, duke prezantuar koncepte të reja ose duke hapur aplikacione të reja komerciale. Shuma e çmimit është 35 mijë dollarë amerikanë. Në vitet e kaluara, çmimet ACM u janë dhënë projekteve GCC dhe LLVM, dhe themeluesve të tyre Richard Stallman dhe Chris Latner. Projekte dhe teknologji të tjera që u shpërblyen gjithashtu ishin UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB dhe eclipse .
Arkitektura e mikrokernelit seL4 është e dukshme për heqjen e pjesëve për menaxhimin e burimeve të kernelit në hapësirën e përdoruesit dhe për aplikimin e të njëjtave mjete të kontrollit të aksesit për burime të tilla si për burimet e përdoruesit. Mikrokerneli nuk ofron abstraksione të nivelit të lartë jashtë kutisë për menaxhimin e skedarëve, proceseve, lidhjeve të rrjetit dhe të ngjashme, në vend të kësaj ai siguron vetëm mekanizma minimalë për kontrollin e aksesit në hapësirën fizike të adresave, ndërprerjet dhe burimet e procesorit. Abstraksionet e nivelit të lartë dhe drejtuesit për ndërveprim me harduerin zbatohen veçmas në krye të mikrokernelit në formën e detyrave të nivelit të përdoruesit. Qasja e detyrave të tilla në burimet në dispozicion të mikrokernelit organizohet përmes përcaktimit të rregullave.
Burimi: opennet.ru