Pas tetë vjet zhvillimi, u lëshua projekti Muen 1.0, duke zhvilluar kernelin Separation, mungesa e gabimeve në kodin burimor të të cilit u konfirmua duke përdorur metoda matematikore të verifikimit formal të besueshmërisë. Kerneli është i disponueshëm për arkitekturën x86_64 dhe mund të përdoret në sistemet kritike për misionin që kërkojnë një nivel më të lartë besueshmërie dhe garanci për asnjë dështim. Kodi burimor i projektit është shkruar në gjuhën Ada dhe në dialektin e saj të verifikueshëm SPARK 2014. Kodi shpërndahet nën licencën GPLv3.
Bërthama e ndarjes është një mikrokernel që siguron një mjedis për ekzekutimin e komponentëve të izoluar nga njëri-tjetri, ndërveprimi i të cilave rregullohet rreptësisht nga rregulla të dhëna. Izolimi bazohet në përdorimin e shtesave të virtualizimit të Intel VT-x dhe përfshin mekanizma sigurie për të bllokuar organizimin e kanaleve të fshehta të komunikimit. Kerneli i ndarjes është më minimalist dhe statik se mikrokernelet e tjerë, gjë që zvogëlon numrin e situatave që mund të shkaktojnë dështim.
Kerneli funksionon në modalitetin rrënjë VMX, i ngjashëm me një hipervizor, dhe të gjithë komponentët e tjerë funksionojnë në modalitetin jo-root VMX, ngjashëm me sistemet e ftuar. Qasja në pajisje bëhet duke përdorur zgjerimet Intel VT-d DMA dhe rimarrëveshjen e ndërprerjes, gjë që bën të mundur zbatimin e lidhjes së sigurt të pajisjeve PCI me komponentët që funksionojnë nën Muen.
Aftësitë e Muen përfshijnë mbështetjen për sistemet me shumë bërthama, faqet e memories së mbivendosur (EPT, Tabelat e Zgjeruara të Faqeve), MSI (Ndërprerjet e sinjalizuara të mesazheve) dhe tabelat e atributeve të faqeve të kujtesës (PAT, Tabela e Atributeve të Faqes). Muen ofron gjithashtu një programues fiks të rrumbullakët bazuar në kohëmatësin parandalues të Intel VMX, një kohë funksionimi kompakt që nuk ndikon në performancën, një sistem auditimi të përplasjeve, një mekanizëm të caktimit të burimeve statike të bazuar në rregulla, një sistem për trajtimin e ngjarjeve dhe kanale memorie të përbashkët për komunikimi brenda komponentëve që funksionojnë.
Ai mbështet funksionimin e komponentëve me kodin e makinës 64-bit, makina virtuale 32 ose 64-bit, aplikacione 64-bit në gjuhët Ada dhe SPARK 2014, makina virtuale Linux dhe "unikernels" të pavarur bazuar në MirageOS në krye të Muen.
Risitë kryesore të ofruara në lëshimin e Muen 1.0:
- Janë publikuar dokumente me specifika për kernelin (pajisja dhe arkitektura), sistemin (politikat e sistemit, Tau0 dhe paketa e veglave) dhe komponentët, të cilat dokumentojnë të gjitha aspektet e projektit.
- Është shtuar paketa e veglave Tau0 (Muen System Composer), e cila përfshin një grup komponentësh të verifikuar të gatshëm për kompozimin e imazheve të sistemit dhe zhvillimin e shërbimeve standarde që funksionojnë në krye të Muen. Komponentët e ofruar përfshijnë drejtuesin AHCI (SATA), Device Manager (DM), ngarkuesin e nisjes, menaxherin e sistemit, terminalin virtual, etj.
- Drejtuesi muenblock Linux (një zbatim i një pajisje blloku që funksionon në krye të memories së përbashkët Muen) është konvertuar për të përdorur API-në e blockdev 2.0.
- Mjete të implementuara për menaxhimin e ciklit jetësor të komponentëve vendas.
- Imazhet e sistemit janë konvertuar për të përdorur SBS (Signed Block Stream) dhe CSL (Command Stream Loader) për të mbrojtur integritetin.
- Është implementuar një drejtues i verifikuar AHCI-DRV, i shkruar në gjuhën SPARK 2014 dhe që ju lejon të lidhni disqet që mbështesin ndërfaqen ATA ose ndarjet individuale të diskut me komponentët.
- Mbështetje e përmirësuar e unikernelit nga projektet MirageOS dhe Solo5.
- Paketa e veglave të gjuhës Ada është përditësuar për publikimin e Komunitetit GNAT 2021.
- Sistemi i integrimit të vazhdueshëm është transferuar nga emulatori Bochs në mjediset e mbivendosura QEMU/KVM.
- Imazhet e komponentit Linux përdorin kernelin Linux 5.4.66.
Burimi: opennet.ru