Представлена платформа для высокозащищенных систем на базе гипервизора seL4

После 7 лет работы Австралийский исследовательский центр NICTA и организация Open Kernel Lab представляют новую систему для обеспечения гарантированного уровня безопасности и отказоустойчивости. С точки зрения разработчиков это стало возможным благодаря:

• Очень малому размеру микроядра-гипервизора и минималистичности функций. Как уже было сказано это микроядро-гипервизор seL4, которое в свою очередь базируется на открытом ядре OKL4 [1]
• Математической проверки кода на устойчивость к сбоям
• Жесткой изоляции процессов друг от друга и от ядра

Разработанная система позиционируется как решение для организации высокобезопасных систем для жизненно важных организаций таких как:

• Медицинские центры(разработчики предлагают ее использовать как ОС для медоборудования )
• Энергетические компании
• Авиационные и другие транспортные компании

Кроме того разработчики считают что в перспективе эта система может послужить хорошей основой для систем электронной коммерции.
Список поддерживаемых архитектур:

• ARM11
• x86
• Запуск в качестве гостя в Linux окружении

Здесь так же следует заметить, что при математическом доказательстве речь идет о проверке того, что система полностью удовлетворяет исходным спецификациям разработчика,следовательно, все равно сохраняются опасности от изначально неправильного проектирования
Исходные тексты, документация доступны для свободного использования, но в некоммерческих целях
Анонс маркетологов [2]
Технические детали [3]

Подробности [3]