Исходное сообщение
"Сверхнадёжное ядро seL4 будет переведено в разряд открытых п..." Отправлено opennews, 25-Июн-14 00:22
Компания 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 (http://ssrg.nicta.com.au/projects/seL4/) (Secure Embedded L4) в категорию открытых проектов.  Ядро seL4 нацелено на предоставление  повышенного уровня безопасности и надёжности для критически важных систем, используемых в авиации, медицине, финансовом секторе, энергетике и других областях, где необходима гарантия отсутствия сбоев. Корректность реализации seL4 в своё время была доказана (http://www.opennet.ru/opennews/art.shtml?num=23011) математически, что даёт основание считать решения на базе seL4 самыми надёжными в мире. 29 июля под одной из свободных лицензий будут не только открыты исходные тексты ядра seL4, но и связанные с системой компоненты доказательства надёжности и сопутствующий код для построения высоконадёжных операционных систем. С технической стороны, ядро seL4 примечательно выносом частей для управления ресурсами ядра в пространство пользователя и применения для таких ресурсов тех же средств разграничения доступа, как для пользовательских ресурсов. Математическое доказательство надёжности свидетельствует о том, что seL4 полностью соответствует заявленным спецификациям и гарантирует отсутствие ошибок, приводящих к проблемам с блокировками, переполнениям буфера, арифметическим исключениям и неинициализированным переменным. URL: https://news.ycombinator.com/item?id=7938149 Новость: http://www.opennet.ru/opennews/art.shtml?num=40075