Выпуск Muen 1.0, открытого микроядра для создания высоконадёжных систем

После восьми лет разработки увидел свет выпуск проекта Muen 1.0, развивающего ядро разделения (Separation kernel), отсутствие ошибок в исходных текстах которого подтверждено при помощи математических методов формальной верификации надёжности. Ядро доступно для архитектуры x86_64 и может применяться в критически важных системах, требующих повышенного уровня надёжности и гарантии отсутствия сбоев. Исходные тексты проекта написаны на языке Ада и его верифицируемом диалекте SPARK 2014. Код распространяется под лицензией GPLv3.

Ядро разделения представляет собой микроядро, предоставляющее окружение для исполнения изолированных друг от друга компонентов, взаимодействие которых жёстко регулируются заданными правилами. Изоляция основана на применении расширений виртуализации Intel VT-x и предусматривает в том числе механизмы защиты для блокировки организации скрытых каналов связи. Ядро разделения более минималистично и статично по сравнению с другими микроядрами, что позволяет сократить число ситуаций, способных привести к сбою.

Ядро выполняется в корневом режиме VMX по аналогии с гипервизором, а всё остальные компоненты в некорневом режиме VMX по аналогии с гостевыми системами. Доступ к оборудованию производится с использованием расширений Intel VT-d DMA и ремаппинга прерываний, что даёт возможность реализовать безопасную привязку PCI-устройств к компонентам, запускаемым под управлением Muen.

Из возможностей Muen отмечается поддержка многоядерных систем, вложенных страниц памяти (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), таблиц атрибутов страниц памяти (PAT, Page Attribute Table). Muen также предоставляет фиксированный цикличный планировщик на базе вытесняющего таймера Intel VMX, компактный runtime, не влияющий на производительность, систему аудита крахов, механизм статического назначения ресурсов на основе правил, систему обработки событий и каналы разделяемой памяти для взаимодействия внутри запускаемых компонентов.

Поддерживается запуск поверх Muen компонентов с 64-разрядным машинным кодом, 32- или 64-разрядных виртуальных машин, 64-разрядных приложений на языках Ada и SPARK 2014, виртуальных машин с Linux и самодостаточных «unikernel» на базе MirageOS.

Основные новшества, предложенные в выпуске Muen 1.0:

• Опубликованы документы со спецификациями ядра (устройство и архитектура), системы (системные политики, Tau0 и инструментарий) и компонентов, в которых документированы все аспекты работы проекта.
• Добавлен инструментарий Tau0 (Muen System Composer), включающий набор готовых верифицированных компонентов для компоновки системных образов и разработки типовых сервисов, запускаемых поверх Muen. Среди предоставляемых компонентов драйвер AHCI (SATA), Device Manager (DM), загрузчик, системный менеджер, виртуальный терминал и т.п.
• Linux-драйвер muenblock (реализация блочного устройства, работающего поверх разделяемой памяти Muen) переведён на использование API blockdev 2.0.
• Реализованы инструменты для управления жизненным циклом нативных компонентов.
• Системные образы переведены на использование SBS (Signed Block Stream) и CSL (Command Stream Loader) для защиты целостности.
• Реализован верифицированный драйвер AHCI-DRV, написанный на языке SPARK 2014 и позволяющий подключать к компонентам накопители, поддерживающие интерфейс ATA, или отдельные дисковые разделы.
• Улучшена поддержка unikernel от проектов MirageOS и Solo5.
• Инструментарий для языка Ада обновлён до выпуска GNAT Community 2021.
• Система непрерывной интеграции переведена с эмулятора Bochs на вложенные окружения QEMU/KVM.
• В образах компонентов с Linux задействовано ядро Linux 5.4.66.

Источник: opennet.ru