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