Исходное сообщение
"Открыт код сверхнадёжного микроядра seL4" Отправлено opennews, 29-Июл-14 09:35
Компания General Dynamics C4 Systems (http://en.wikipedia.org/wiki/General_Dynamics_C4_Systems)&nb...и австралийский исследовательский центр NICTA (http://en.wikipedia.org/wiki/NICTA) открыли (http://sel4.systems/) под свободными лицензиями исходные тексты микроядра seL4 (https://github.com/seL4/seL4) (Secure Embedded L4), компоненты (https://github.com/seL4/l4v) математического доказательства его надёжности и сопутствующий код для построения высоконадёжных операционных систем. Ядро открыто (https://github.com/seL4) под лицензией GPLv2, а утилиты и работающий в пространстве пользователя код содержит как элементы под лицензией GPLv2, так и компоненты под лицензией BSD. Микроядро seL4 нацелено на предоставление  повышенного уровня безопасности и надёжности для критически важных систем, используемых в авиации, медицине, финансовом секторе, энергетике и других областях, где необходима гарантия отсутствия сбоев. Корректность реализации seL4 в своё время была доказана (http://www.opennet.ru/opennews/art.shtml?num=23011) математически, что даёт основание считать решения на базе seL4 самыми надёжными в мире. Математическое доказательство надёжности свидетельствует о том, что seL4 полностью соответствует заданным на формальном языке спецификациям и гарантирует отсутствие ошибок, приводящих к проблемам с блокировками, переполнениям буфера, арифметическим исключениям и неинициализированным переменным. В своё время Агентство по перспективным оборонным научно-исследовательским разработкам США (DARPA) использовало seL4 для повышения защищённости ПО, используемого в военных беспилотных летательных аппаратах. Архитектура seL4 примечательна (http://sel4.systems/FAQ/) выносом частей для управления ресурсами ядра в пространство пользователя и применения для таких ресурсов тех же средств разграничения доступа, как для пользовательских ресурсов. Для разработчиков предлагается компоненто-ориентированная платформа для разработки приложений CAmkES (http://sel4.systems/CAmkES/), позволяющая моделировать и создавать системы на основе seL4 в виде коллекции взаимодействующих между собой компонентов. Также поставляется (https://github.com/seL4) набор примеров и прототипов систем на основе seL4, подборка драйверов и библиотека для создания драйверов, порт  Си-библиотеки Musl (http://www.opennet.ru/opennews/art.shtml?num=39365). URL: https://github.com/seL4 Новость: http://www.opennet.ru/opennews/art.shtml?num=40297