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

[Dmitry Shurupov]

29 июля 2014 года будет открыт исходный код операционной системы seL4, созданной Австралийским национальным центром информационных и коммуникационных систем (NICTA) и американской компанией General Dynamics C4 Systems. seL4 microkernel представляет собой компактное микроядро третьего поколения на базе L4. Код написан на языке C и состоит из 8700 строк. По словам представителей NICTA, seL4 подходит для использования в смартфонах, военных системах, медицинском оборудовании и беспилотных устройствах и летательных аппаратах. seL4 обладает полной «гарантией функциональной точности», и данная реализация соответствует этим спецификациям. Кроме того, двоичный код, выполняемый на оборудовании правильно транслируется в код C, а это значит, что компилятору не стоит доверять и функциональная точность проверяется для бинарного кода. По мнению NICTA, это обеспечивает отсутствие ошибок в операционной системе, целостность и конфиденциальность. Сайт проекта — sel4.systems.

оригинал на www.nixp.ru