Ядро seL4 – раскрытие кода

25. June 2014, 8:57 Безопасность, Компьютеры и ПО, Ссылки

Вот здесь, используя один из новых доменов верхнего уровня (.systems), объявляют о том, что раскроют исходные коды (и сопутствующую информацию – см. ниже) микроядра seL4. Главная особенность данного ядра ОС в том, что его реализация прошла через процедуру формального доказательства её соответствия спецификации. То есть, доказано, что в реализации отсутствуют некоторые классы типичных ошибок и уязвимостей. (Пишут, что всё это касается версии ядра для архитектуры ARM, и что seL4 – первое ядро, прошедшее подобную проверку.)

Вообще, доказательства отсутствия программных ошибок – это штука, весьма полезная для современного состояния дел с разработкой ПО. Тем более, когда речь идёт о разных встроенных устройствах, которых так много вокруг. Можно помечтать: в будущем все операционные системы и прикладное ПО будут проходить “формальную верификацию” и ошибки в них исчезнут. Почему? Да потому, что успешное прохождение верификации означает, что для всех багов строго доказано – это не баги, а “фичи”.

Адрес записки: https://dxdt.ru/2014/06/25/6852/

Похожие записки:



Далее - мнения и дискуссии

(Сообщения ниже добавляются читателями сайта, через форму, расположенную в конце страницы.)

Комментарии читателей блога: 5

  • 1. 25th June 2014, 13:16 // Читатель sarin написал:

    и наступит мир во всём мире.

    как это всё соотносится с теоремой Гёделя? кто выполняет проверку соответствия спецификации?

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

  • 2. 25th June 2014, 21:24 // Читатель jno написал:

    ну, с бортовым ПО в авиации такое уже некоторое время происходит…
    да, по причине “зависона” самолёты пока не падали.
    но та же убогость древних протоколов никуда не делась.

  • 3. 26th June 2014, 00:27 // Читатель Jeff Zanooda написал:

    Строго говоря, Гёдель тут не при чём. Из того, что существуют правильные программы, правильность которых не может быть доказана не следует, что не может быть доказана правильность конкретно seL4.

    Другое дело что особого смысла в этой деятельности я не вижу. Программа все равно будет делать, что я сказал, а не что я имел в виду. А сказал я это в спецификации или в коде – это уже не так важно.

  • 4. 27th June 2014, 11:44 // Читатель sarin написал:

    такая верификация могла бы очень сильно сократить затраты на тестирование продукта. если достоверно известно, что ПО абсолютно точно соответствует спецификации то расхождения со спекой можно уже не искать.

  • 5. 27th June 2014, 21:33 // Читатель Jeff Zanooda написал:

    Расходы на тестирование сократятся, зато расходы на написание спецификации возрастут. Вордовый документ или даже RFC скормить процедуре формального доказательства не получится.