SeL4 avoin mikroydinprojekti on saanut ACM Software System Award -palkinnon, joka on vuosittain arvostetuimman tietokonejärjestelmien alan kansainvälisen järjestön Association for Computing Machinery (ACM) myöntämä palkinto. Palkinto myönnetään saavutuksista matemaattisen toiminnan todistamisen alalla, mikä osoittaa täydellistä noudattamista virallisella kielellä annettujen spesifikaatioiden kanssa ja tunnustaa valmiuden käytettäväksi toiminnan kannalta kriittisissä sovelluksissa. SeL4-projekti on osoittanut, että projektien luotettavuus ja tietoturva on täysin muodollisesti mahdollista varmentaa teollisten käyttöjärjestelmien tasolla, vaan myös saavuttaa suorituskyvystä ja monipuolisuudesta tinkimättä.
ACM Software System Award jaetaan vuosittain tunnustuksena toimialaan ratkaisevasti vaikuttaneiden ohjelmistojärjestelmien kehittämiselle, uusien konseptien käyttöönotolle tai kaupallisten sovellusten avaamiselle. Palkinnon suuruus on 35 tuhatta Yhdysvaltain dollaria. Viime vuosina ACM-palkintoja on jaettu GCC- ja LLVM-projekteille sekä niiden perustajille Richard Stallmanille ja Chris Latnerille. Muita palkittuja projekteja ja teknologioita olivat UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB ja eclipse .
Mikroytimen seL4:n arkkitehtuuri on huomionarvoinen osien poistamisesta ytimen resurssien hallintaa varten käyttäjätilassa ja samojen pääsynvalvontamenetelmien soveltamisesta tällaisiin resursseihin kuin käyttäjäresursseihin. Mikroydin ei tarjoa valmiita korkean tason abstraktioita tiedostojen, prosessien, verkkoyhteyksien ja vastaavien hallintaan, vaan se tarjoaa vain minimaalisia mekanismeja fyysisen osoiteavaruuden, keskeytysten ja prosessoriresurssien käytön hallitsemiseksi. Korkean tason abstraktiot ja ajurit laitteiston kanssa vuorovaikutusta varten toteutetaan erikseen mikroytimen päälle käyttäjätason tehtävien muodossa. Tällaisten tehtävien pääsy mikroytimen käytettävissä oleviin resursseihin on järjestetty sääntöjen määrittelyn kautta.
Lähde: opennet.ru