Na acht jaar ontwikkeling werd het Muen 1.0-project uitgebracht, waarbij de Separation-kernel werd ontwikkeld, waarvan de afwezigheid van fouten in de broncode werd bevestigd met behulp van wiskundige methoden voor formele betrouwbaarheidsverificatie. De kernel is beschikbaar voor de x86_64-architectuur en kan worden gebruikt in bedrijfskritische systemen die een hoger niveau van betrouwbaarheid en garantie op geen storingen vereisen. De broncode van het project is geschreven in de Ada-taal en het verifieerbare dialect SPARK 2014. De code wordt gedistribueerd onder de GPLv3-licentie.
De scheidingskernel is een microkernel die een omgeving biedt voor de uitvoering van van elkaar geïsoleerde componenten, waarvan de interactie strikt wordt gereguleerd door bepaalde regels. Isolatie is gebaseerd op het gebruik van Intel VT-x virtualisatie-uitbreidingen en omvat beveiligingsmechanismen om de organisatie van geheime communicatiekanalen te blokkeren. De partitiekernel is minimalistischer en statischer dan andere microkernels, waardoor het aantal situaties dat storingen kan veroorzaken, wordt verminderd.
De kernel draait in de VMX-rootmodus, vergelijkbaar met een hypervisor, en alle andere componenten draaien in de VMX-niet-rootmodus, vergelijkbaar met gastsystemen. Toegang tot de apparatuur vindt plaats met behulp van Intel VT-d DMA-extensies en interrupt-remapping, wat het mogelijk maakt om veilige binding van PCI-apparaten aan componenten die onder Muen draaien te implementeren.
De mogelijkheden van Muen omvatten ondersteuning voor multi-core systemen, geneste geheugenpagina's (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) en geheugenpagina-attribuuttabellen (PAT, Page Attribute Table). Muen biedt ook een vaste round-robin-planner op basis van de preventieve timer van Intel VMX, een compacte runtime die geen invloed heeft op de prestaties, een crash-auditsysteem, een op regels gebaseerd mechanisme voor het toewijzen van statische bronnen, een gebeurtenisafhandelingssysteem en gedeelde geheugenkanalen voor communicatie binnen actieve componenten.
Het ondersteunt actieve componenten met 64-bit machinecode, 32- of 64-bit virtuele machines, 64-bit applicaties in Ada- en SPARK 2014-talen, virtuele Linux-machines en op zichzelf staande “unikernels” gebaseerd op MirageOS bovenop Muen.
De belangrijkste innovaties die worden aangeboden in de release van Muen 1.0:
- Er zijn documenten gepubliceerd met specificaties voor de kernel (apparaat en architectuur), het systeem (systeembeleid, Tau0 en toolkit) en componenten, die alle aspecten van het project documenteren.
- De Tau0 (Muen System Composer) toolkit is toegevoegd, die een reeks kant-en-klare, geverifieerde componenten bevat voor het samenstellen van systeemimages en het ontwikkelen van standaardservices die bovenop Muen draaien. De meegeleverde componenten zijn onder meer een AHCI (SATA)-stuurprogramma, Device Manager (DM), bootloader, systeembeheer, virtuele terminal, enz.
- Het muenblock Linux-stuurprogramma (een implementatie van een blokapparaat dat bovenop het gedeelde Muen-geheugen draait) is geconverteerd om de blockdev 2.0 API te gebruiken.
- Tools geïmplementeerd voor het beheren van de levenscyclus van native componenten.
- Systeemimages zijn geconverteerd om SBS (Signed Block Stream) en CSL (Command Stream Loader) te gebruiken om de integriteit te beschermen.
- Er is een geverifieerd AHCI-DRV-stuurprogramma geïmplementeerd, geschreven in de SPARK 2014-taal waarmee u schijven die de ATA-interface ondersteunen of individuele schijfpartities op de componenten kunt aansluiten.
- Verbeterde unikernel-ondersteuning van MirageOS- en Solo5-projecten.
- De Ada-taaltoolkit is bijgewerkt voor de GNAT Community 2021-release.
- Het continue integratiesysteem is overgebracht van de Bochs-emulator naar geneste QEMU/KVM-omgevingen.
- Linux-componentimages gebruiken de Linux 5.4.66-kernel.
Bron: opennet.ru