Проекту seL4 присуждена премия ACM Software System Award

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