Проект, що розвиває відкрите мікроядро 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