Po ôsmich rokoch vývoja sa spustila verzia projektu Muen 1.0, ktorá sa zaoberá jadrom rozdelenia (Separation kernel), pričom absencia chýb v zdrojových kódoch bola potvrdená matematickými metódami formálnej verifikácie spoľahlivosti. Jadro je dostupné pre architektúru x86_64 a môže sa používať v kritických systémoch, ktoré si vyžadujú zvýšenú úroveň spoľahlivosti a záruku absencie porúch. Zdrojové kódy projektu sú napísané v programovacom jazyku Ada a jeho verifikovateľnom dialekte SPARK 2014. Kód sa distribuuje pod licenciou GPLv3.
Jadro rozdelenia predstavuje mikrojadro, ktoré poskytuje prostredie pre spúšťanie izolovaných komponentov, ktorých interakcia je prísne regulovaná stanovenými pravidlami. Izolácia je založená na použití rozšírení virtualizácie Intel VT-x a predpokladá aj mechanizmy ochrany na blokovanie skrytých komunikačných kanálov. Jadro rozdelenia je minimalistickejšie a statickejšie v porovnaní s inými mikrojadrami, čo umožňuje znížiť počet situácií, ktoré môžu viesť k poruche.
Jadro beží v koreňovom režime VMX podobne ako hypervízor, zatiaľ čo všetky ostatné komponenty bežia v nekoreňovom režime VMX podobne ako hosťujúce systémy. Prístup k hardvéru sa uskutočňuje pomocou rozšírení Intel VT-d DMA a premapovania prerušenia, čo umožňuje bezpečné prepojenie PCI zariadení na komponenty spravované Muen.
Medzi schopnosti Muen patrí podpora viacjadrových systémov, vnorené stránky pamäte (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), tabuľky atribútov strán pamäte (PAT, Page Attribute Table). Muen tiež poskytuje fixovaný cyklický plánovač založený na pretláčacom časovači Intel VMX, kompaktný runtime, ktorý neovplyvňuje výkon, systém auditu zlyhaní, mechanizmus statického pridelovania zdrojov na základe pravidiel, systém spracovania udalostí a kanály zdieľanej pamäte na interakciu v rámci spúšťaných komponentov.
Podporuje spúšťanie komponentov s 64-bitovým strojovým kódom, 32- alebo 64-bitových virtuálních strojů, 64-bitových aplikácií v jazykoch Ada a SPARK 2014, virtuálnych strojov s Linuxom a samostatných „unikernel“ na báze MirageOS.
Hlavné novinky, ktoré prináša vydanie Muen 1.0:
- Boli zverejnené dokumenty so špecifikáciami jadra (zariadenie a architektúra), systému (systémové politiky, Tau0 a nástroje) a komponentmi, ktoré dokumentujú všetky aspekty fungovania projektu.
- Bol pridaný nástroj Tau0 (Muen System Composer), ktorý obsahuje sadu ready-to-use verifikovaných komponentov na kompozíciu systémových obrazov a vývoj typových služieb, ktoré sa spúšťajú nad Muen. Medzi dostupnými komponentmi sú ovládač AHCI (SATA), Device Manager (DM), bootloader, systémový manažér, virtuálny terminál a podobne.
- Linuxový ovládač muenblock (realizácia blokového zariadenia, ktoré pracuje nad zdieľanou pamäťou Muen) bol prevedený na používanie API blockdev 2.0.
- Boli implementované nástroje na správu životného cyklu natívnych komponentov.
- Systémové obrazy boli prevedené na využívanie SBS (Signed Block Stream) a CSL (Command Stream Loader) na ochranu integrity.
- Bol implementovaný verifikovaný ovládač AHCI-DRV, napísaný v jazyku SPARK 2014, ktorý umožňuje pripojiť k komponentom úložiská podporujúce rozhranie ATA alebo jednotlivé diskové oddiely.
- Zlepšená podpora unikernel z projektov MirageOS a Solo5.
- Nástroje pre jazyk Ada boli aktualizované na vydanie GNAT Community 2021.
- Systém kontinuálnej integrácie bol prevedený z emulátora Bochs na vnorené prostredia QEMU/KVM.
- V obrazových komponentoch s Linuxom bolo použitých jadro Linux 5.4.66.
Zdroj: opennet.ru
