Projektet, der udvikler den åbne mikrokerne seL4, har modtaget ACM Software System Award, som årligt uddeles af Association for Computing Machinery (ACM), den mest autoritative internationale organisation inden for computersystemer. Prisen blev givet for præstationer inden for matematisk bevis for driftspålidelighed, hvilket indikerer fuld overholdelse af specifikationer givet i et formelt sprog og anerkender paratheden til brug i kritiske applikationer. seL4-projektet har vist, at det ikke kun er muligt at udføre fuldt formel verifikation af pålidelighed og sikkerhed for projekter på niveau med industrielle operativsystemer, men også at opnå dette uden at ofre ydeevne og alsidighed.
ACM Software System Award uddeles årligt for at anerkende softwaresystemer, der har haft en afgørende indflydelse på en branche ved at introducere nye koncepter eller åbne op for nye kommercielle anvendelsesområder. Prisen er på 35 amerikanske dollars. I tidligere år er ACM-priser blevet givet til GCC- og LLVM-projekterne og deres grundlæggere Richard Stallman og Chris Latner. Andre projekter og teknologier, der er blevet tildelt priser, omfatter UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB og Eclipse.
seL4-mikrokernens arkitektur er bemærkelsesværdig ved dens fjernelse af dele til styring af kerneressourcer ind i brugerområdet og ved brugen af de samme midler til adgangskontrol for sådanne ressourcer som for brugerressourcer. Mikrokernen leverer ikke færdige abstraktioner på højt niveau til styring af filer, processer, netværksforbindelser osv., men i stedet kun minimale mekanismer til styring af adgang til det fysiske adresseområde, afbrydelser og processorressourcer. Abstraktioner på højt niveau og drivere til interaktion med hardwaren implementeres separat oven på mikrokernen i form af opgaver, der udføres på brugerniveau. Adgang for sådanne opgaver til de ressourcer, der er tilgængelige for mikrokernen, er organiseret ved at definere regler.
Kilde: opennet.ru
