Projekt vyvíjajúci otvorené mikrokernel seL4 získal ocenenie ACM Software System Award, ktoré každoročne udeľuje Asociácia pre výpočtové stroje (ACM), najuznávanejšia medzinárodná organizácia v oblasti počítačových systémov. Cena sa udeľuje za úspechy v oblasti matematického dôkazu spoľahlivosti prevádzky, ktorý preukazuje úplnú zhodu so špecifikáciami uvedenými vo formálnom jazyku a uznáva pripravenosť na použitie v kritických aplikáciách. Projekt seL4 ukázal, že nielenže je možné plne formálne overiť spoľahlivosť a bezpečnosť pre návrhy priemyselných operačných systémov, ale tiež to dosiahnuť bez kompromisov vo výkone a všestrannosti.
Ocenenie ACM Software System Award sa udeľuje každoročne ako ocenenie za vývoj softvérových systémov, ktoré majú rozhodujúci vplyv na priemysel, zavádzajú nové koncepty alebo otvárajú nové oblasti komerčného využitia. Výška ocenenia je 35-tisíc amerických dolárov. V minulých rokoch boli ceny ACM udelené projektom GCC a LLVM a ich zakladateľom Richardovi Stallmanovi a Chrisovi Latnerovi. Ocenenie ocenilo aj projekty a technológie ako UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB a Eclipse .
Architektúra mikrojadra seL4 sa vyznačuje presúvaním častí na správu zdrojov jadra do užívateľského priestoru a využívaním rovnakých nástrojov na riadenie prístupu k takýmto zdrojom ako k užívateľským zdrojom. Mikrokernel neposkytuje hotové abstrakcie na vysokej úrovni pre správu súborov, procesov, sieťových pripojení a podobne, namiesto toho poskytuje len minimálne mechanizmy na riadenie prístupu k fyzickému adresnému priestoru, prerušeniam a zdrojom procesora. Vysokoúrovňové abstrakcie a ovládače pre interakciu s hardvérom sú implementované oddelene na vrchole mikrojadra vo forme úloh na užívateľskej úrovni. Prístup takýchto úloh k zdrojom dostupným pre mikrokernel je organizovaný prostredníctvom definície pravidiel.
Zdroj: opennet.ru