Проектът, който развива отвореното микроядро 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
