Пускане на Muen 1.0, отворено микроядро за изграждане на високонадеждни системи

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

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

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

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

Той поддържа работещи компоненти с 64-битов машинен код, 32- или 64-битови виртуални машини, 64-битови приложения на езиците Ada и SPARK 2014, Linux виртуални машини и самостоятелни „единични ядра“, базирани на MirageOS върху Muen.

Основните иновации, предлагани в изданието на Muen 1.0:

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

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