Після восьми років розробки побачив світ випуск проекту 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