Исходный код «самой надёжной в мире ОС» seL4 microkernel будет открыт через месяц

29 июля 2014 года будет открыт исходный код операционной системы seL4, созданной Австралийским национальным центром информационных и коммуникационных систем (NICTA) и американской компанией General Dynamics C4 Systems.

Отсчёт времени до публикации исходного кода на сайте sel4 / Иллюстрация с сайта nixp.ru

seL4 microkernel представляет собой компактное микроядро третьего поколения на базе L4. Код написан на языке C и состоит из 8700 строк. По словам представителей NICTA, seL4 подходит для использования в смартфонах, военных системах, медицинском оборудовании и беспилотных устройствах и летательных аппаратах.

seL4 обладает полной «гарантией функциональной точности», и данная реализация соответствует этим спецификациям. Кроме того, двоичный код, выполняемый на оборудовании правильно транслируется в код C, а это значит, что компилятору не стоит доверять и функциональная точность проверяется для бинарного кода. По мнению NICTA, это обеспечивает отсутствие ошибок в операционной системе, целостность и конфиденциальность.

Сайт проекта — sel4.systems.

Автор: Никита Лялин по материалам TechWorld Australia.