Det åpne mikrokjerneprosjektet seL4 har mottatt ACM Software System Award, en årlig pris gitt av Association for Computing Machinery (ACM), den mest respekterte internasjonale organisasjonen innen datasystemer. Prisen gis for prestasjoner innen matematisk bevis på operasjon, som indikerer full overholdelse av spesifikasjoner gitt på et formelt språk og anerkjenner beredskap for bruk i virksomhetskritiske applikasjoner. seL4-prosjektet har vist at det ikke bare er mulig å fullt ut formelt verifisere pålitelighet og sikkerhet for prosjekter på nivå med industrielle operativsystemer, men også å oppnå dette uten å ofre ytelse og allsidighet.
ACM Software System Award deles ut årlig for å anerkjenne utviklingen av programvaresystemer som har hatt en avgjørende innvirkning på bransjen, introduserer nye konsepter eller åpner nye kommersielle applikasjoner. Prisbeløpet er 35 tusen amerikanske dollar. I de siste årene har ACM-priser blitt gitt til GCC- og LLVM-prosjektene, og deres grunnleggere Richard Stallman og Chris Latner. Andre prosjekter og teknologier som har blitt anerkjent inkluderer UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB og Eclipse.
Arkitekturen til seL4 mikrokjernen er kjent for fjerning av deler for å administrere kjerneressurser i brukerrommet og for å bruke de samme midlene for tilgangskontroll for slike ressurser som for brukerressurser. Mikrokjernen gir ikke ut-av-boksen høynivåabstraksjoner for å administrere filer, prosesser, nettverkstilkoblinger og lignende, i stedet gir den bare minimale mekanismer for å kontrollere tilgang til det fysiske adresserommet, avbrudd og prosessorressurser. Abstraksjoner på høyt nivå og drivere for samhandling med maskinvare implementeres separat på toppen av mikrokjernen i form av oppgaver på brukernivå. Tilgangen til slike oppgaver til ressursene som er tilgjengelige for mikrokjernen er organisert gjennom definisjonen av regler.
Kilde: opennet.ru