Avatud mikrokerneli projekt seL4 on pälvinud ACM Software System Awardi, iga-aastase auhinna, mille annab välja arvutisüsteemide valdkonna tunnustatuim rahvusvaheline organisatsioon Association for Computing Machinery (ACM). Auhind antakse saavutuste eest matemaatilise töötõenduse valdkonnas, mis näitab täielikku vastavust ametlikus keeles antud spetsifikatsioonidele ja tunnustab valmisolekut kasutamiseks missioonikriitilistes rakendustes. Projekt seL4 on näidanud, et projektide usaldusväärsust ja turvalisust ei ole võimalik mitte ainult täielikult formaalselt kontrollida tööstuslike operatsioonisüsteemide tasemel, vaid ka seda saavutada ilma jõudlust ja mitmekülgsust ohverdamata.
ACM tarkvarasüsteemi auhinda antakse välja igal aastal, et tunnustada tarkvarasüsteemide arendamist, millel on olnud tööstusele määrav mõju, uute kontseptsioonide juurutamine või uute kommertsrakenduste avamine. Preemia suurus on 35 tuhat USA dollarit. Viimastel aastatel on ACM-i auhindu saanud GCC ja LLVM projektid ning nende asutajad Richard Stallman ja Chris Latner. Auhind on antud ka sellistele projektidele ja tehnoloogiatele nagu UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB ja Eclipse.
Mikrokerneli seL4 arhitektuur on tähelepanuväärne selle poolest, et kasutajaruumis on eemaldatud osad kerneli ressursside haldamiseks ja selliste ressursside jaoks samade juurdepääsukontrolli vahendite rakendamisega nagu kasutajaressursside jaoks. Mikrotuum ei paku valmis kõrgetasemelisi abstraktsioone failide, protsesside, võrguühenduste ja muu sarnase haldamiseks, selle asemel pakub see ainult minimaalseid mehhanisme juurdepääsu kontrollimiseks füüsilisele aadressiruumile, katkestustele ja protsessori ressurssidele. Kõrgetasemelised abstraktsioonid ja draiverid riistvaraga suhtlemiseks rakendatakse mikrokerneli peale eraldi kasutajataseme ülesannete kujul. Selliste ülesannete juurdepääs mikrokernelile kättesaadavatele ressurssidele on korraldatud reeglite määratlemise kaudu.
Allikas: opennet.ru