Po ôsmich rokoch vývoja bol vydaný projekt Muen 1.0 vyvíjajúci jadro Separation, ktorého absencia chýb v zdrojovom kóde bola potvrdená pomocou matematických metód formálneho overovania spoľahlivosti. Jadro je k dispozícii pre architektúru x86_64 a možno ho použiť v kritických systémoch, ktoré vyžadujú zvýšenú úroveň spoľahlivosti a záruky bez porúch. Zdrojový kód projektu je napísaný v jazyku Ada a jeho overiteľnom dialekte SPARK 2014. Kód je šírený pod licenciou GPLv3.
Separačné jadro je mikrokernel, ktorý poskytuje prostredie na vykonávanie komponentov izolovaných od seba, ktorých interakcia je prísne regulovaná danými pravidlami. Izolácia je založená na použití virtualizačných rozšírení Intel VT-x a zahŕňa bezpečnostné mechanizmy na blokovanie organizácie skrytých komunikačných kanálov. Rozdeľovacie jadro je minimalistickejšie a statickejšie ako iné mikrojadrá, čo znižuje počet situácií, ktoré môžu spôsobiť zlyhanie.
Jadro beží v koreňovom režime VMX, podobnom hypervízoru, a všetky ostatné komponenty bežia v režime bez oprávnenia typu VMX, podobne ako hosťujúce systémy. Prístup k zariadeniu je zabezpečený pomocou rozšírení Intel VT-d DMA a premapovania prerušení, čo umožňuje implementovať zabezpečenú väzbu PCI zariadení na komponenty bežiace pod Muen.
Možnosti Muen zahŕňajú podporu pre viacjadrové systémy, vnorené pamäťové stránky (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) a tabuľky atribútov pamäťových stránok (PAT, Page Attribute Table). Muen tiež poskytuje pevný plánovač typu round-robin založený na preemptívnom časovači Intel VMX, kompaktný runtime, ktorý neovplyvňuje výkon, systém auditovania zlyhaní, mechanizmus prideľovania statických zdrojov založený na pravidlách, systém spracovania udalostí a kanály zdieľanej pamäte pre komunikácia v rámci bežiacich komponentov.
Podporuje spustené komponenty so 64-bitovým strojovým kódom, 32- alebo 64-bitové virtuálne stroje, 64-bitové aplikácie v jazykoch Ada a SPARK 2014, virtuálne stroje Linux a samostatné „unikernely“ založené na MirageOS nad Muen.
Hlavné inovácie ponúkané vo vydaní Muen 1.0:
- Boli publikované dokumenty so špecifikáciami pre jadro (zariadenie a architektúra), systém (systémové politiky, Tau0 a sada nástrojov) a komponenty, ktoré dokumentujú všetky aspekty projektu.
- Bola pridaná súprava nástrojov Tau0 (Muen System Composer), ktorá obsahuje sadu hotových overených komponentov na skladanie systémových obrazov a vývoj štandardných služieb, ktoré bežia nad Muen. Medzi poskytované komponenty patrí ovládač AHCI (SATA), Správca zariadení (DM), zavádzač, správca systému, virtuálny terminál atď.
- Linuxový ovládač muenblock (implementácia blokového zariadenia bežiaceho nad zdieľanou pamäťou Muen) bol konvertovaný na používanie blockdev 2.0 API.
- Implementované nástroje na riadenie životného cyklu natívnych komponentov.
- Systémové obrazy boli skonvertované na používanie SBS (Signed Block Stream) a CSL (Command Stream Loader) na ochranu integrity.
- Implementovaný bol overený ovládač AHCI-DRV napísaný v jazyku SPARK 2014 a umožňujúci ku komponentom pripojiť jednotky podporujúce rozhranie ATA alebo jednotlivé diskové partície.
- Vylepšená podpora unikernelu z projektov MirageOS a Solo5.
- Jazyková sada nástrojov Ada bola aktualizovaná pre vydanie komunity GNAT 2021.
- Systém nepretržitej integrácie bol prenesený z emulátora Bochs do vnorených prostredí QEMU/KVM.
- Obrazy komponentov Linuxu používajú jadro Linuxu 5.4.66.
Zdroj: opennet.ru