Представлена платформа для высокозащищенных систем на базе гипервизора seL4
После 7 лет работы Австралийский исследовательский центр NICTA и организация Open Kernel Lab представляют новую систему для обеспечения гарантированного уровня безопасности и отказоустойчивости. С точки зрения разработчиков это стало возможным благодаря:
- Очень малому размеру микроядра-гипервизора и минималистичности функций. Как уже было сказано это микроядро-гипервизор seL4, которое в свою очередь базируется на открытом ядре OKL4
- Математической проверки кода на устойчивость к сбоям
- Жесткой изоляции процессов друг от друга и от ядра
Разработанная система позиционируется как решение для организации высокобезопасных систем для жизненно важных организаций таких как:
- Медицинские центры(разработчики предлагают ее использовать как ОС для медоборудования )
- Энергетические компании
- Авиационные и другие транспортные компании
Кроме того разработчики считают что в перспективе эта система может послужить хорошей основой для систем электронной коммерции.
Список поддерживаемых архитектур:
- ARM11
- x86
- Запуск в качестве гостя в Linux окружении
Здесь так же следует заметить, что при математическом доказательстве речь идет о проверке того, что система полностью удовлетворяет исходным спецификациям разработчика,следовательно, все равно сохраняются опасности от изначально неправильного проектирования
Исходные тексты, документация доступны для свободного использования, но в некоммерческих целях
Анонс маркетологов
Технические детали