Efter otte års udvikling blev Muen 1.0-projektet frigivet, der udviklede Separation-kernen, hvis fravær af fejl i kildekoden blev bekræftet ved hjælp af matematiske metoder til formel pålidelighedsverifikation. Kernen er tilgængelig til x86_64-arkitekturen og kan bruges i missionskritiske systemer, der kræver et øget niveau af pålidelighed og garanti for fejl. Projektets kildekode er skrevet på Ada-sproget og dets verificerbare dialekt SPARK 2014. Koden distribueres under GPLv3-licensen.
Separationskernen er en mikrokerne, der giver et miljø til udførelse af komponenter isoleret fra hinanden, hvis interaktion er strengt reguleret af givne regler. Isolering er baseret på brugen af Intel VT-x virtualiseringsudvidelser og inkluderer sikkerhedsmekanismer til at blokere organiseringen af hemmelige kommunikationskanaler. Partitioneringskernen er mere minimalistisk og statisk end andre mikrokerner, hvilket reducerer antallet af situationer, der kan forårsage fejl.
Kernen kører i VMX root-tilstand, svarende til en hypervisor, og alle andre komponenter kører i VMX non-root-tilstand, svarende til gæstesystemer. Adgang til udstyret sker ved hjælp af Intel VT-d DMA-udvidelser og interrupt remapping, som gør det muligt at implementere sikker binding af PCI-enheder til komponenter, der kører under Muen.
Muens muligheder omfatter understøttelse af multi-core-systemer, indlejrede hukommelsessider (EPT, Extended Page Tables), MSI (Message Signaled Interrupts) og hukommelsessideattributtabeller (PAT, Page Attribute Table). Muen leverer også en fast round-robin skemalægger baseret på Intel VMX forebyggende timer, en kompakt kørselstid, der ikke påvirker ydeevnen, et nedbrudskontrolsystem, en regelbaseret statisk ressourcetildelingsmekanisme, et hændelseshåndteringssystem og delte hukommelseskanaler for kommunikation inden for kørende komponenter.
Det understøtter kørende komponenter med 64-bit maskinkode, 32- eller 64-bit virtuelle maskiner, 64-bit applikationer i Ada og SPARK 2014 sprog, virtuelle Linux maskiner og selvstændige "unikernels" baseret på MirageOS oven på Muen.
De vigtigste nyskabelser, der tilbydes i udgivelsen af Muen 1.0:
- Der er udgivet dokumenter med specifikationer for kernen (enhed og arkitektur), system (systempolitikker, Tau0 og værktøjssæt) og komponenter, som dokumenterer alle aspekter af projektet.
- Tau0 (Muen System Composer) værktøjssættet er blevet tilføjet, som inkluderer et sæt færdige verificerede komponenter til at komponere systembilleder og udvikle standardtjenester, der kører oven på Muen. De medfølgende komponenter inkluderer AHCI (SATA) driver, Device Manager (DM), boot loader, system manager, virtuel terminal osv.
- Muenblock Linux-driveren (en implementering af en blokenhed, der kører oven på Muen-delte hukommelse) er blevet konverteret til at bruge blockdev 2.0 API.
- Implementerede værktøjer til styring af livscyklussen for native komponenter.
- Systembilleder er blevet konverteret til at bruge SBS (Signed Block Stream) og CSL (Command Stream Loader) for at beskytte integriteten.
- En verificeret AHCI-DRV-driver er blevet implementeret, skrevet i SPARK 2014-sproget og giver dig mulighed for at tilslutte drev, der understøtter ATA-interfacet eller individuelle diskpartitioner til komponenterne.
- Forbedret unikernel-understøttelse fra MirageOS- og Solo5-projekter.
- Ada-sprogværktøjssættet er blevet opdateret til GNAT Community 2021-udgivelsen.
- Det kontinuerlige integrationssystem er blevet overført fra Bochs-emulatoren til QEMU/KVM-indlejrede miljøer.
- Linux-komponentbilleder bruger Linux 5.4.66-kernen.
Kilde: opennet.ru