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