Po osmi letech vývoje byl vydán projekt Muen 1.0 vyvíjející jádro Separation, jehož absence chyb ve zdrojovém kódu byla potvrzena pomocí matematických metod formálního ověřování spolehlivosti. Jádro je k dispozici pro architekturu x86_64 a lze jej použít v kritických systémech, které vyžadují zvýšenou úroveň spolehlivosti a záruku, že nedojde k selhání. Zdrojový kód projektu je napsán v jazyce Ada a jeho ověřitelném dialektu SPARK 2014. Kód je šířen pod licencí GPLv3.
Separační jádro je mikrokernel, který poskytuje prostředí pro provádění vzájemně izolovaných komponent, jejichž interakce je přísně regulována danými pravidly. Izolace je založena na použití virtualizačních rozšíření Intel VT-x a zahrnuje bezpečnostní mechanismy pro blokování organizace skrytých komunikačních kanálů. Rozdělovací jádro je minimalističtější a statičtější než jiná mikrojádra, což snižuje počet situací, které mohou způsobit selhání.
Jádro běží v režimu VMX root, podobně jako hypervisor, a všechny ostatní komponenty běží v režimu VMX non-root, podobně jako hostující systémy. Přístup k zařízení je zajištěn pomocí rozšíření Intel VT-d DMA a přemapování přerušení, což umožňuje implementovat zabezpečenou vazbu zařízení PCI na komponenty běžící pod Muen.
Možnosti Muen zahrnují podporu pro vícejádrové systémy, vnořené paměťové stránky (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) a tabulky atributů paměťových stránek (PAT, Page Attribute Table). Muen také poskytuje pevný plánovač typu round-robin založený na preemptivním časovači Intel VMX, kompaktní běhové prostředí, které neovlivňuje výkon, systém auditování zhroucení, mechanismus přidělování statických zdrojů založený na pravidlech, systém zpracování událostí a kanály sdílené paměti pro komunikace v rámci běžících komponent.
Podporuje běžící komponenty s 64bitovým strojovým kódem, 32bitové nebo 64bitové virtuální stroje, 64bitové aplikace v jazycích Ada a SPARK 2014, virtuální stroje Linux a samostatné „unikernely“ založené na MirageOS nad Muenem.
Hlavní inovace nabízené ve verzi Muen 1.0:
- Byly zveřejněny dokumenty se specifikacemi pro jádro (zařízení a architektura), systém (systémové zásady, Tau0 a sada nástrojů) a komponenty, které dokumentují všechny aspekty projektu.
- Byla přidána sada nástrojů Tau0 (Muen System Composer), která obsahuje sadu hotových ověřených komponent pro skládání obrazů systému a vývoj standardních služeb, které běží nad Muenem. Mezi poskytované komponenty patří ovladač AHCI (SATA), Správce zařízení (DM), zavaděč, správce systému, virtuální terminál atd.
- Linuxový ovladač muenblock (implementace blokového zařízení běžícího nad sdílenou pamětí Muen) byl převeden na blockdev 2.0 API.
- Implementované nástroje pro řízení životního cyklu nativních komponent.
- Systémové obrazy byly převedeny na použití SBS (Signed Block Stream) a CSL (Command Stream Loader) k ochraně integrity.
- Byl implementován ověřený ovladač AHCI-DRV napsaný v jazyce SPARK 2014 a umožňující ke komponentám připojit disky podporující rozhraní ATA nebo jednotlivé diskové oddíly.
- Vylepšená podpora unikernelu z projektů MirageOS a Solo5.
- Jazyková sada nástrojů Ada byla aktualizována pro vydání komunity GNAT 2021.
- Systém kontinuální integrace byl převeden z emulátoru Bochs do vnořených prostředí QEMU/KVM.
- Obrazy součástí Linuxu používají jádro Linux 5.4.66.
Zdroj: opennet.ru