Efter åtta års utveckling släpptes Muen 1.0-projektet, som utvecklade Separation-kärnan, vars frånvaro av fel i källkoden bekräftades med matematiska metoder för formell tillförlitlighetsverifiering. Kärnan är tillgänglig för x86_64-arkitekturen och kan användas i verksamhetskritiska system som kräver en ökad nivå av tillförlitlighet och garanti för att inga fel uppstår. Källkoden för projektet är skriven på Ada-språket och dess verifierbara dialekt SPARK 2014. Koden distribueras under GPLv3-licensen.
Separationskärnan är en mikrokärna som tillhandahåller en miljö för exekvering av komponenter isolerade från varandra, vars interaktion är strikt reglerad av givna regler. Isolering är baserad på användningen av Intel VT-x virtualiseringstillägg och inkluderar säkerhetsmekanismer för att blockera organisationen av hemliga kommunikationskanaler. Partitioneringskärnan är mer minimalistisk och statisk än andra mikrokärnor, vilket minskar antalet situationer som kan orsaka fel.
Kärnan körs i VMX-rotläge, liknande en hypervisor, och alla andra komponenter körs i VMX icke-rootläge, liknande gästsystem. Åtkomst till utrustningen görs med hjälp av Intel VT-d DMA-tillägg och interrupt remapping, vilket gör det möjligt att implementera säker bindning av PCI-enheter till komponenter som körs under Muen.
Muens möjligheter inkluderar stöd för flerkärniga system, kapslade minnessidor (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) och minnessideattributtabeller (PAT, Page Attribute Table). Muen tillhandahåller också en fast round-robin-schemaläggare baserad på Intel VMX-förebyggande timer, en kompakt körtid som inte påverkar prestandan, ett kraschrevisionssystem, en regelbaserad statisk resurstilldelningsmekanism, ett händelsehanteringssystem och delade minneskanaler för kommunikation inom löpande komponenter.
Den stöder körande komponenter med 64-bitars maskinkod, 32- eller 64-bitars virtuella maskiner, 64-bitars applikationer i Ada och SPARK 2014-språk, virtuella Linux-maskiner och fristående "unikernels" baserade på MirageOS ovanpå Muen.
De viktigaste innovationerna som erbjuds i utgåvan av Muen 1.0:
- Dokument har publicerats med specifikationer för kärnan (enhet och arkitektur), system (systempolicyer, Tau0 och verktygslåda) och komponenter, som dokumenterar alla aspekter av projektet.
- Verktygssatsen Tau0 (Muen System Composer) har lagts till, som innehåller en uppsättning färdiga verifierade komponenter för att komponera systembilder och utveckla standardtjänster som körs ovanpå Muen. Komponenter som tillhandahålls inkluderar AHCI (SATA) drivrutin, Device Manager (DM), starthanterare, systemhanterare, virtuell terminal, etc.
- Muenblock Linux-drivrutinen (en implementering av en blockenhet som körs ovanpå det delade Muen-minnet) har konverterats för att använda blockdev 2.0 API.
- Implementerade verktyg för att hantera livscykeln för inbyggda komponenter.
- Systembilder har konverterats till att använda SBS (Signed Block Stream) och CSL (Command Stream Loader) för att skydda integriteten.
- En verifierad AHCI-DRV-drivrutin har implementerats, skriven på SPARK 2014-språket och låter dig ansluta enheter som stöder ATA-gränssnittet eller enskilda diskpartitioner till komponenterna.
- Förbättrat unikernelstöd från MirageOS- och Solo5-projekten.
- Ada-språkverktygssatsen har uppdaterats för GNAT Community 2021-utgåvan.
- Det kontinuerliga integrationssystemet har överförts från Bochs-emulatorn till QEMU/KVM-kapslade miljöer.
- Linux-komponentavbildningar använder Linux 5.4.66-kärnan.
Källa: opennet.ru