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