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