SeL4 öppna mikrokärnprojektet har fått ACM Software System Award, en årlig utmärkelse som ges av Association for Computing Machinery (ACM), den mest respekterade internationella organisationen inom området datorsystem. Priset ges för prestationer inom området matematiska bevis på drift, vilket indikerar full överensstämmelse med specifikationer som ges på ett formellt språk och erkänner beredskap för användning i verksamhetskritiska tillämpningar. seL4-projektet har visat att det inte bara är möjligt att helt formellt verifiera tillförlitlighet och säkerhet för projekt på nivå med industriella operativsystem, utan också att uppnå detta utan att ge avkall på prestanda och mångsidighet.
ACM Software System Award delas ut årligen för att uppmärksamma utvecklingen av mjukvarusystem som har haft en avgörande inverkan på branschen, infört nya koncept eller öppnat upp nya kommersiella applikationer. Priset är 35 tusen US-dollar. Under de senaste åren har ACM-priser delats ut till GCC- och LLVM-projekten och deras grundare Richard Stallman och Chris Latner. Andra projekt och teknologier som också belönades var UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB och eclipse .
Arkitekturen för mikrokärnan seL4 är anmärkningsvärd för borttagningen av delar för att hantera kärnresurser i användarutrymmet och för att tillämpa samma sätt för åtkomstkontroll för sådana resurser som för användarresurser. Mikrokärnan tillhandahåller inte out-of-the-box abstraktioner på hög nivå för hantering av filer, processer, nätverksanslutningar och liknande, istället tillhandahåller den endast minimala mekanismer för att kontrollera åtkomst till det fysiska adressutrymmet, avbrott och processorresurser. Abstraktioner på hög nivå och drivrutiner för interaktion med hårdvara implementeras separat ovanpå mikrokärnan i form av uppgifter på användarnivå. Tillgången för sådana uppgifter till de resurser som är tillgängliga för mikrokärnan organiseras genom definition av regler.
Källa: opennet.ru