Na acht jaar ontwikkeling is de release van het Muen 1.0-project een feit, dat de core separation (scheidingkernel) ontwikkelt, waarvan de afwezigheid van fouten in de bronbestanden is bevestigd met behulp van mathematische methoden voor formele verificatie van betrouwbaarheid. De kernel is beschikbaar voor de x86_64-architectuur en kan worden toegepast in kritieke systemen die een verhoogd niveau van betrouwbaarheid vereisen en garanties bieden voor het ontbreken van storingen. De bronbestanden van het project zijn geschreven in de Ada-taal en zijn verifieerbare dialect SPARK 2014. De code wordt verspreid onder de GPLv3-licentie.
De scheidingkernel is een microkernel die een omgeving biedt voor de uitvoering van van elkaar geĆÆsoleerde componenten, waarvan de interactie streng wordt gereguleerd door vastgestelde regels. De isolatie is gebaseerd op het gebruik van Intel VT-x virtualisatie-extensies en omvat ook mechanismen voor bescherming tegen het creĆ«ren van verborgen communicatiekanalen. De scheidingkernel is minimalistisch en statisch in vergelijking met andere microkernels, wat het aantal situaties dat tot een storing kan leiden vermindert.
De kernel draait in VMX-rootmodus, vergelijkbaar met een hypervisor, en alle andere componenten in non-root VMX-modus, vergelijkbaar met gastsystemen. Toegang tot de hardware wordt verkregen met behulp van Intel VT-d DMA-extensies en interrupt-remapping, wat veilige binding van PCI-apparaten aan componenten die onder Muen draaien mogelijk maakt.
Onder de mogelijkheden van Muen wordt de ondersteuning voor multicore-systemen, geneste paginatabellen (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), en paginattributentabellen (PAT, Page Attribute Table) benadrukt. Muen biedt ook een vaste cyclusplaner op basis van de preemptive timer van Intel VMX, een compacte runtime die de prestaties niet beĆÆnvloedt, een crashaudit-systeem, een mechanisme voor statische toewijzing van middelen op basis van regels, een gebeurtenisverwerkingsysteem en kanalen voor gedeeld geheugen voor interactie binnen de draaiende componenten.
Het is mogelijk om Muen-componenten te draaien met 64-bits machinecode, 32- of 64-bits virtuele machines, 64-bits toepassingen in de talen Ada en SPARK 2014, virtuele machines met Linux en zelfstandige "unikernel" op basis van MirageOS.
De belangrijkste vernieuwingen die in de release van Muen 1.0 zijn voorgesteld:
- Documenten met specificaties van de kernel (structuur en architectuur), systeem (systeembeleid, Tau0 en hulpprogramma's) en componenten zijn gepubliceerd, waarin alle aspecten van het project zijn gedocumenteerd.
- Het hulpprogramma Tau0 (Muen System Composer) is toegevoegd, inclusief een set kant-en-klare, geverifieerde componenten voor het samenstellen van systeeme beelden en het ontwikkelen van standaarddiensten die bovenop Muen draaien. Onder de meegeleverde componenten bevinden zich de AHCI (SATA)-driver, Device Manager (DM), bootloader, systeembeheerder, virtuele terminal, enzovoort.
- De Linux-driver muenblock (implementatie van een blokapparaat dat werkt bovenop gedeeld geheugen van Muen) is overgezet naar het gebruik van API blockdev 2.0.
- Er zijn tools geĆÆmplementeerd voor het beheer van de levenscyclus van native componenten.
- Systeems afbeeldingen zijn overgezet naar het gebruik van SBS (Signed Block Stream) en CSL (Command Stream Loader) ter bescherming van de integriteit.
- Een geverifieerde AHCI-DRV-driver is geĆÆmplementeerd, geschreven in de programmeertaal SPARK 2014, die het mogelijk maakt om ATA-compatibele opslagapparaten of afzonderlijke schijf partities aan de componenten te koppelen.
- De ondersteuning voor unikernels van de projecten MirageOS en Solo5 is verbeterd.
- De toolset voor de Ada-taal is bijgewerkt naar de uitgave van GNAT Community 2021.
- Het systeem voor continue integratie is overgezet van de Bochs-emulator naar geneste omgevingen QEMU/KVM.
- In de componentbeelden met Linux is kernel Linux 5.4.66 gebruikt.
Bron: opennet.ru
