Pärast kaheksat aastat arendust nägi päevavalgust projekt Muen 1.0, mis arendab välja eraldamise (Separation kernel) põhijõudu, mille allika tekstide vigu kinnitavad formaalse verifitseerimise matemaatilised meetodid. Südamik on saadaval arhitektuuril x86_64 ja seda saab kasutada kriitilistes süsteemides, mis nõuavad suurenenud usaldusväärsust ja tõrgete puudumise garantiid. Projekti lähtekood on kirjutatud Ada keeles ja selle valideeritavas diaklektis SPARK 2014. Kood jaotatakse GPLv3 litsentsi all.
Eraldussüdamik on mikroühend, mis pakub isoleeritud komponentide täitmise keskkonda, mille vaheline suhtlemine on rangelt reguleeritud ettenähtud reeglite järgi. Isolatsioon põhineb Intel VT-x virtualiseerimise laienduste rakendamisel ja hõlmab ka kaitsemehhanisme varjatud suhtluskanalite blokeerimiseks. Eraldussüdamik on võrreldes teiste mikroühenditega minimalistlikum ja staatilisem, mis vähendab tõrgete võimalike olukordade arvu.
Südamik töötab VMX juurerežiimis sarnaselt hüperviisoriga, samas kui kõik muud komponendid töötavad VMX mittejuurerežiimis, sarnaselt külalis süsteemidega. Ligipääs riistvarale toimub Intel VT-d DMA laienduste ja katkemise ümbersuunamise kaudu, mis võimaldab rakendada ohutut PCI-seadmete sidumist Muen'i haldamisel käituvate komponentidega.
Muen toob esile mitme tuuma süsteemide, sissetunginud mälu lehtede (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), mälu lehtede atribuutide tabelite (PAT, Page Attribute Table) toe. Muen pakub ka fikseeritud tsüklilist ajakava Intel VMX'i sunniviisilise ajastija baasil, kompaktset runtime'i, mis ei mõjuta tulemuslikkust, rikete auditeerimise süsteemi, reeglite põhjalikku ressursside staatilist määramist, sündmuste töötlemise süsteemi ja jagatud mälu kanaleid käitatavate komponentide vaheliseks suhtlemiseks.
Muen toetab 64-bitise masinkoodi, 32- või 64-bitiste rakenduste käitamist, virtuaalmasinate, 64-bitiste rakenduste käitamist Ada ja SPARK 2014 keeltes, Linuxi virtuaalmasinaid ja iseseisvaid “unikernel” lahendusi MirageOS baasil.
Peamised uuendused, mis on pakutud Muen 1.0 väljalaskes:
- Avaldatud on dokumentatsioon tuumade (seade ja arhitektuur), süsteemide (süsteemipoliitikad, Tau0 ja tööriistakomplekt) ja komponentide spetsifikatsioonide kohta, kus on dokumenteeritud kõik projekti tööd puudutavad aspektid.
- Lisatud on tööriistakomplekt Tau0 (Muen System Composer), mis sisaldab valmis kinnitatud komponente süsteemipiltide koostamiseks ja tüüpteenuste arendamiseks, mis töötavad Muen'i peal. Pakutavate komponentide seas on AHCI (SATA) draiver, Seadmese haldur (DM), buutijuhend, süsteemihaldur, virtuaalne terminal jne.
- Linuxi draiver muenblock (plokiseadmise teostus, mis töötab Muen'i jagatud mälu peal) on ümber suunatud API blockdev 2.0 kasutamisele.
- Reaalsete komponentide elutsükli haldamiseks on teostatud tööriistad.
- Süsteemipildid on ümber suunatud SBS (Signed Block Stream) ja CSL (Command Stream Loader) kasutamisele, et kaitsta terviklikkust.
- Teostatud on kinnitatud AHCI-DRV draiver, kirjutatud SPARK 2014 keeles, mis võimaldab ühendada komponendiga ATA-t toetavaid salvestusseadmeid või eraldi ketas jagusid.
- Unikerneli tugi projektidest MirageOS ja Solo5 on paranenud.
- Ada keele tööriistakomplekti on uuendatud GNAT Community 2021 versioonini.
- Jätkuva integreerimise süsteem on üle viidud emulaatorilt Bochs QEMU/KVM sisesesse keskkonda.
- Linuxi komponentide piltides on kasutatud Linuxi tuuma versioon 5.4.66.
Allikas: opennet.ru
