Сверхнадёжное ядро seL4 будет переведено в разряд открытых проектов
Компания General Dynamics C4 Systems и австралийский исследовательский центр NICTA анонсировали скорый перевод микроядра seL4 (Secure Embedded L4) в категорию открытых проектов. Ядро seL4 нацелено на предоставление повышенного уровня безопасности и надёжности для критически важных систем, используемых в авиации, медицине, финансовом секторе, энергетике и других областях, где необходима гарантия отсутствия сбоев. Корректность реализации seL4 в своё время была доказана математически, что даёт основание считать решения на базе seL4 самыми надёжными в мире. 29 июля под одной из свободных лицензий будут не только открыты исходные тексты ядра seL4, но и связанные с системой компоненты доказательства надёжности и сопутствующий код для построения высоконадёжных операционных систем. С технической стороны, ядро seL4 примечательно выносом частей для управления ресурсами ядра в пространство пользователя и применения для таких ресурсов тех же средств разграничения доступа, как для пользовательских ресурсов. Математическое доказательство надёжности свидетельствует о том, что seL4 полностью соответствует заявленным спецификациям и гарантирует отсутствие ошибок, приводящих к проблемам с блокировками, переполнениям буфера, арифметическим исключениям и неинициализированным переменным.
© OpenNet
