Projektet, der udvikler den åbne seL4-mikrokerne, modtog ACM Software System Award, der uddeles årligt af Association for Computing Machinery (ACM), den mest autoritative internationale organisation inden for computersystemer. Prisen tildeles for præstationer inden for matematisk bevis på driftsikkerhed, som demonstrerer fuld overensstemmelse med specifikationer specificeret i et formelt sprog og anerkender parathed til brug i missionskritiske applikationer. seL4-projektet har vist, at det ikke kun er muligt fuldt ud formelt at verificere pålidelighed og sikkerhed for design på industrielt styresystemniveau, men også at opnå dette uden at gå på kompromis med ydeevne og alsidighed.
ACM Software System Award uddeles årligt for at anerkende udviklingen af softwaresystemer, der har haft en afgørende indflydelse på industrien, introducerer nye koncepter eller åbner op for nye områder inden for kommerciel anvendelse. Prisen er på 35 tusinde amerikanske dollars. I de seneste år er ACM-priser blevet tildelt GCC- og LLVM-projekterne og deres grundlæggere Richard Stallman og Chris Latner. Prisen anerkendte også projekter og teknologier som UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB og Eclipse .
Arkitekturen af seL4-mikrokernen er bemærkelsesværdig for bevægelige dele til styring af kerneressourcer til brugerrum og brug af de samme adgangskontrolværktøjer til sådanne ressourcer som for brugerressourcer. Mikrokernen leverer ikke færdige abstraktioner på højt niveau til styring af filer, processer, netværksforbindelser og lignende; i stedet giver den kun minimale mekanismer til at kontrollere adgang til fysisk adresserum, afbrydelser og processorressourcer. Abstraktioner på højt niveau og drivere til interaktion med hardware implementeres separat oven på mikrokernen i form af opgaver på brugerniveau. Adgang til sådanne opgaver til de ressourcer, der er tilgængelige for mikrokernen, organiseres gennem definition af regler.
Kilde: opennet.ru