Projektet som utvecklar det öppna mikrokärnan seL4 har tilldelats ACM Software System Award, som årligen utdelas av Association for Computing Machinery (ACM), den mest ansedda internationella organisationen inom datorsystem. Utmärkelsen ges för prestationer inom matematisk bevisning av systemets pålitlighet, vilket visar full överensstämmelse med de specificerade formella språken och bekräftar dess beredskap för kritiska tillämpningar. Projektet seL4 har visat att det är möjligt att helt formellt verifiera pålitlighet och säkerhet för industrialiserade operativsystem utan att påverka prestanda och flexibilitet.
ACM Software System Award delas årligen ut för utveckling av programvarusystem som haft en avgörande inverkan på branschen genom att införa nya koncept eller avslöja nya områden för kommersiell tillämpning. Prissumman är 35 000 US-dollar. Tidigare har ACM-priserna tilldelats projekten GCC och LLVM, samt deras grundare Richard Stallman och Chris Lattner. Andra hedrade projekt och teknologier inkluderar 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 mikroarkitekturen seL4 kännetecknas av att man flyttar delar av kärnans resurskontroll till användarutrymmet och tillämpar samma åtkomstkontrollmetoder för dessa resurser som för användarresurser. Mikroarkitekturen tillhandahåller ingen färdig hög-nivå-abstraktion för hantering av filer, processer, nätverksanslutningar osv., utan ger endast minimala mekanismer för att hantera åtkomsten till det fysiska adressutrymmet, avbrott och processorresurser. Högnivåabstraktioner och drivrutiner för interaktion med hårdvara implementeras separat ovanpå mikroarkitekturen i form av uppgifter som körs på användarnivå. Åtkomsten för sådana uppgifter till mikroarkitekturens resurser organiseras genom fastställande av regler.
Källa: opennet.ru
