Семейство микроядер L4 для встроенных систем пополнилось микроядром seL4, созданным с расчётом на применение в критически важных системах, где отказ оборудования недопустим. Это беспилотные летательные аппараты и медицинские приборы. Но использовать новое микроядро можно абсолютно в любых устройствах, поскольку оно отличается рекордной производительностью: автомобили, самолёты, современное оружие и многое другое.
Микроядро не контролирует высокоуровневые процессы доступа к файлам, процессам и т.д. Оно только управляет доступом к физическому адресному пространству, прерываниям и процессору. Все остальные конструкции строятся поверх этого и работают в соответствии с заданными правилами. Новинка отличается строгой изоляцией процессов: все системные драйверы, процессы и прочее перенесено в user space, код открыт и проверен на безопасность.
На практике это означает, что беспилотник с операционной системой на микроядре seL4 трудно вывести из строя стандартными методами. Если обычному БПЛА в воздухе поступит сигнал от «командного центра» завершить работу ОС, то он выключится и разобьётся (такие диверсии со стороны противника уже были). А вот разработчики нового микроядра провели демонстрацию, как беспилотник с seL4, получив такую команду, просто моргает светодиодными фонарями и улетает.
По результатам тестирования, seL4 обеспечивает максимальную производительность среди всех существующих микроядер. Правда, разработчики оговариваются, что такие результаты получены при помощи микрооптимизаций ядра, которые пока держатся в секрете. Опубликованная в открытом доступе версия ядра на 10-20% медленнее, хотя и в этом случае seL4 показывает непревзойдённую производительность. По крайней мере, среди тех микроядер, которые открыто публиковали результаты тестов.
Проект разработан учёными австралийского института NICTA при финансировании DARPA, помощи опытных инженеров и математиков Boeing, Rockwell Collins и других компаний. Авторы опубликовали исходный код и формальное математическое доказательство защищённости ядра.
SeL4 работает на ARMv6 (ARM11), ARMv7 (Cortex A8, A9, A15) и x86. Поддерживаемые ARM-платформы: Freescale i.MX31, OMAP3 BeagleBoard, Exynos Arndale 5250, Odroid-X, Odroid-XU, Inforce IFC6410 и Freescale i.MX6 Sabre Lite. Среди x86-совместимых поддерживаются абсолютно все устройства, на таких процессорах даже можно запустить Linux на микроядре seL4, при поддержке технологии виртуализации Intel VT-x.
