nixp.ru v3.0

11 декабря 2016,
воскресенье,
14:52:53 MSK

DevOps с компанией «Флант»
18 июня 2014, 15:13

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

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

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

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

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

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

Постоянная ссылка к новости: https://www.nixp.ru/news/12557.html. Никита Лялин по материалам TechWorld Australia.

fb twitter vk
rgo

> Кроме того, двоичный код, выполняемый на оборудовании правильно транслируется в код C, а это значит, что компилятору не стоит доверять и функциональная точность проверяется для бинарного кода.

Нашёл в оригинале исходную фразу:

seL4 has full ‘functional correctness proof’, so the implementation (written in C) adheres to its specification. Also, the binary code that executes on the hardware is a correct translation of the C code, meaning that the compiler does not have to be trusted and extends the functional correctness property to the binary.

Могу предложить более адекватный перевод, как минимум он точнее:

sel4 имеет полное «доказательство функциональной корректности», то есть доказательство того, что реализация (написанная на C) точно соответствует спецификациям. Кроме того, двоичный код, выполняемый на оборудовании является точной трансляцией кода на C, что гарантируется тем, что разработчики не доверяют компилятору и выполняют проверку функциональной точности ещё и для бинарного кода.

Помимо коррекции общего смысла в нюансах кто куда транслируется, в этом переводе я перевожу слово «proof» словом «доказательство», что довольно-таки критично, поскольку речь, очевидно, идёт именно о том, чтобы строго доказать корректность кода. Задача, вообще, не из лёгких, но когда очень хочется, и когда строк кода всего 8700, видимо возможно.

Дмитрий Шурупов

Спасибо большое, подредактировал!

ecobeingecobeing.ru
Экология и вегетарианство на благо всем живым существам Планеты.