Проектът за отворено микроядро seL4 получи наградата ACM Software System Award, годишна награда, присъждана от Асоциацията за компютърни машини (ACM), най-уважаваната международна организация в областта на компютърните системи. Наградата се дава за постижения в областта на математическото доказателство за работа, което показва пълно съответствие със спецификациите, дадени на официален език, и признава готовността за използване в критични приложения. Проектът seL4 показа, че не само е възможно напълно формално да се провери надеждността и сигурността за проекти на ниво индустриални операционни системи, но и да се постигне това, без да се жертва производителността и гъвкавостта.
Наградата ACM Software System Award се връчва ежегодно, за да признае развитието на софтуерни системи, които са имали определящо въздействие върху индустрията, въвеждайки нови концепции или откривайки нови търговски приложения. Размерът на наградата е 35 хиляди щатски долара. През последните години наградите на ACM бяха дадени на проектите GCC и LLVM и техните основатели Ричард Столман и Крис Латнър. Други проекти и технологии, които също бяха наградени, бяха UNIX, Java, Apache, Mosaic, WWW, Smalltalk, PostScript, TeX, Tcl/Tk, RPC, Make, DNS, AFS, Eiffel, VMware, Wireshark, Jupyter Notebooks, Berkeley DB и eclipse .
Архитектурата на микроядрото seL4 се отличава с премахването на части за управление на ресурсите на ядрото в потребителското пространство и за прилагане на същите средства за контрол на достъпа за такива ресурси, както за потребителските ресурси. Микроядрото не предоставя готови абстракции на високо ниво за управление на файлове, процеси, мрежови връзки и други подобни, вместо това предоставя само минимални механизми за контролиране на достъпа до физическото адресно пространство, прекъсванията и ресурсите на процесора. Абстракциите на високо ниво и драйверите за взаимодействие с хардуера се изпълняват отделно върху микроядрото под формата на задачи на потребителско ниво. Достъпът на такива задачи до ресурсите, достъпни за микроядрото, се организира чрез дефиниране на правила.
Източник: opennet.ru