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

След осем години разработка, проектът Muen 1.0, който развива ядрото за разделяне (Separation kernel), най-накрая е факт. Отсъствието на грешки в изходния код е потвърдено чрез математически методи за официална верификация на надеждността. Ядрото е налично за архитектурата x86_64 и може да се прилага в критични системи, изискващи висок уровень на надеждност и гаранция за отсъствие на сривове. Изходният код на проекта е написан на езика Ada и неговия верифицируем диалект 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, който не влияе на производителността, система за одит на сривовете, механизъм за статично разпределение на ресурсите на базата на правила, система за обработка на събития и канали за споделена памет за взаимодействие между стартираните компоненти.

Поддържа се стартиране на компоненти с 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 е подобрена.
• Инструменти за езика Ada са актуализирани до версия GNAT Community 2021.
• Системата за непрекъсната интеграция е преведена от емулатора Bochs на вложени среди QEMU/KVM.
• В образите на компонентите с Linux е внедрено ядрото Linux 5.4.66.

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