Произведен выпуск раздельного ядра (раздельное ядро) Muen, разрабатываемого швейцарской компанией Codelabs.
Muen поддерживает только платформы Intel x86_64 и обеспечивает гарантии, что запущенные в нем ядра ОС и приложения не могут получать доступ к ресурсам сверх выделенной квоты. Это касается, в том числе, оперативной памяти, процессорного времени и доступа к устройствам ввода-вывода.
В качестве гостевых приложений поддерживаются ядро Linux, программы на Ada/SPARK, а также библиотечные ОС, написанные с использованием фреймворка Solo5 (например, MirageOS на OCaml). Для Linux предоставлены драйверы ядра для ускорения доступа к PCI и другим ресурсам хоста.
Сам Muen целиком реализован на SPARK – безопасном подмножестве языка Ada – и прошел верификацию на отсутствие ошибок времени выполнения. Код распространяется под лицензией GPLv3.
Източник: linux.org.ru
