Projektet, der udvikler det åbne mikro-kernel seL4, har modtaget ACM Software System Award, som årligt tildeles af Association for Computing Machinery (ACM), den mest anerkendte internationale organisation inden for computersystemer. Prisen gives for præstationer inden for matematisk bevis for driftsikkerhed, hvilket beviser fuld overensstemmelse med de formaliserede specifikationer og anerkender beredskabet til brug i kritiske anvendelser. Projektet seL4 har vist, at det er muligt ikke kun at udføre en komplet formel verificering af driftsikkerhed og sikkerhed for projekter på niveau med industrielle operativsystemer, men også at opnå dette uden at gå på kompromis med ydeevne og alsidighed.
ACM Software System Award tildeles årligt for udviklingen af software-systemer, der har haft en væsentlig indflydelse på branchen, ved at introdusere nye koncepter eller afdække nye områder af kommerciel anvendelse. Prisen er 35.000 USD. Tidligere har priserne ACM været tildelt projekter som GCC og LLVM, samt deres stiftere Richard Stallman og Chris Lattner. Prisen har også anerkendt sådanne 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.
Mikro-arkitekturen seL4 er bemærkelsesværdig for at flytte dele til kernekontrol af ressourcer til brugerens rum og anvende de samme adgangsgrænsningsmetoder til sådanne ressourcer som til brugerressourcer. Mikro-kernen tilbyder ikke foruddefinerede høj-niveau abstraktioner til håndtering af filer, processer, netværksforbindelser osv.; i stedet giver den kun minimale mekanismer til at styre adgangen til fysisk adresseområde, afbrydelser og processoressourcer. Høj-niveau abstraktioner og drivere til interaktion med hardware implementeres separat oven på mikro-kernen som opgaver, der kører på bruger-niveau. Adgangen for disse opgaver til de ressourcer, mikro-kernen råder over, organiseres gennem definering af regler.
Kilde: opennet.ru
