Po osmi letech vývoje byl uveden projekt Muen 1.0, který vyvíjí jádro oddělení (Separation kernel), jehož absence chyb v zdrojových textech byla potvrzena matematickými metodami formální verifikace spolehlivosti. Jádro je dostupné pro architekturu x86_64 a může být použito v kritických systémech, vyžadujících zvýšenou úroveň spolehlivosti a záruku absence selhání. Zdrojové texty projektu jsou napsány v jazyce Ada a jeho verifikovatelné variantě SPARK 2014. Kód je distribuován pod licencí GPLv3.
Jádro oddělení představuje mikro-jádro, které poskytuje prostředí pro provádění izolovaných komponent, jejichž interakce jsou přísně regulovány stanovenými pravidly. Izolace je založena na použití rozšíření virtualizace Intel VT-x a zahrnuje také mechanismy ochrany k blokování organizace skrytých komunikačních kanálů. Jádro oddělení je minimalističtější a statičtější než ostatní mikro-jádra, což umožňuje snížit počet situací, které by mohly vést k selhání.
Jádro běží v kořenovém režimu VMX, obdobně jako hypervizor, zatímco všechny ostatní komponenty běží v nekorenovém režimu VMX, obdobně jako hostitelské systémy. Přístup k hardwaru se realizuje pomocí rozšíření Intel VT-d DMA a přemapování přerušení, což umožňuje bezpečné přiřazení PCI zařízení k komponentám, které běží pod správou Muen.
Mezi možnosti Muen patří podpora vícejádrových systémů, vložených stránek paměti (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), tabulek atributů stránek paměti (PAT, Page Attribute Table). Muen také poskytuje pevný cyklický plánovač založený na vyhazovacím časovači Intel VMX, kompaktní runtime, který neovlivňuje výkon, systém auditu selhání, mechanismus statického přiřazení zdrojů na základě pravidel, systém zpracování událostí a kanály sdílené paměti pro interakci mezi spuštěnými komponentami.
Podporuje se spuštění komponent s 64bitovým strojovým kódem, 32bitových nebo 64bitových virtuálních strojů, 64bitových aplikací ve funkcích Ada a SPARK 2014, virtuálních strojích s Linuxem a samostatných "unikernel" na bázi MirageOS.
Hlavní novinky, které byly zavedeny ve vydání Muen 1.0:
- Byly zveřejněny dokumenty se specifikacemi jádra (architektura a struktura), systému (systémové politiky, Tau0 a nástroje) a komponent, ve kterých jsou zdokumentovány všechny aspekty fungování projektu.
- Byly přidány nástroje Tau0 (Muen System Composer), které zahrnují sadu připravených a ověřených komponent pro sestavení systémových obrazů a vývoj typických služeb spouštěných nad Muen. Mezi poskytovanými komponentami jsou ovladač AHCI (SATA), správce zařízení (DM), zavaděč, systémový manažer, virtuální terminál atd.
- Linuxový ovladač muenblock (implementace blokového zařízení fungujícího nad sdílenou pamětí Muen) byl převeden na použití API blockdev 2.0.
- Byly realizovány nástroje pro správu životního cyklu nativních komponent.
- Systémové obrazy byly převedeny na použití SBS (Signed Block Stream) a CSL (Command Stream Loader) pro ochranu integrity.
- Byl implementován ověřený ovladač AHCI-DRV, napsaný v jazyce SPARK 2014, který umožňuje připojení úložných zařízení podporujících rozhraní ATA nebo jednotlivých diskových oddílů.
- Byla vylepšena podpora unikernelů z projektů MirageOS a Solo5.
- Nástroje pro jazyk Ada byly aktualizovány na verzi GNAT Community 2021.
- Systém kontinuální integrace byl převeden z emulátoru Bochs na vnořené prostředí QEMU/KVM.
- V obrazech komponent s Linuxem bylo použito jádro Linux 5.4.66.
Zdroj: opennet.ru
