Издание Muen 1.0, отворено микроядро за създаване на високо надеждни системи

След осем години разработка, проектираният проект Muen 1.0, разширяващ ядрото за разделяне, беше пуснат. Отсъствието на грешки в изходните текстове е потвърдено с математически методи за формална верификация на надеждността. Ядрото е достъпно за архитектура x86_64 и може да се използва в критично важни системи, изискващи повишен niveau на надеждност и гарантирана липса на сривове. Изходните текстове на проекта са написани на езика Ada и неговият верифицируем диалект SPARK 2014. Кодът се разпространява под лицензия GPLv3.

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

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

От възможностите на Muen се отбелязва поддръжката на многоядрени системи, вложени страници на паметта (EPT, Разширени Таблици на Страници), MSI (Прекъсвания, сигнализирани от съобщения), таблици на атрибутите на страниците на паметта (PAT, Таблица на Атрибутите на Страниците). Muen също предлага фиксиран цикличен планировчик на базата на изключващ таймер Intel VMX, компактен runtime, който не влияе на производителността, система за одит на сривове, механизъм за статично разпределение на ресурсите на базата на правила, система за обработка на събития и канали за споделена памет за взаимодействие между стартираните компоненти.

Поддържа се стартиране на компоненти с 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