Pas tetë vjetësh zhvillimi, doli në dritë lëshimi i projektit Muen 1.0, i cili zhvillon kernelin e ndarjes (Separation kernel), ku mungesa e gabimeve në tekstin e burimit është konfirmuar përmes metodave matematikore të verifikimit formal të besueshmërisë. Kernel-i është në dispozicion për arkitekturën x86_64 dhe mund të përdoret në sisteme kritike që kërkojnë një nivel më të lartë besueshmërie dhe garanci të mungesës së dështimeve. Tekstet e burimit të projektit janë shkruar në gjuhën Ada dhe në dialektin e saj të verifikueshëm SPARK 2014. Kodi shpërndahet nën licencën GPLv3.
Kernel-i i ndarjes përfaqëson një mikrokernel që ofron një mjedis për ekzekutimin e komponenteve të izoluara nga njëra-tjetra, me ndërveprimin e tyre të rregulluar rrigorisht nga rregulla të caktuara. Izolimi bazohet në përdorimin e zgjerimeve të virtualizimit Intel VT-x dhe parashikon, ndër të tjera, mekanizma mbrojtës për bllokimin e organizimit të kanaleve të fshehta të komunikimit. Kernel-i i ndarjes është më minimal dhe statik në krahasim me mikrokernelet e tjera, duke lejuar kështu uljen e numrit të situatave që mund të çojnë në dështim.
Kernel-i ekzekutohet në modin rrënjësor VMX, në mënyrë të ngjashme me hipervizorin, ndërsa të gjitha komponentët e tjerë ekzekutohen në modin jo rrënjësor VMX, si sistemi i mysafirëve. Qasja në harduer realizohet duke përdorur zgjerimet Intel VT-d DMA dhe rimappingun e ndërprerjeve, gjë që mundëson realizimin e lidhjes së sigurt të pajisjeve PCI me komponentët që ekzekutohen nën menaxhimin e Muen.
Në mesin e mundësive të Muen është mbështetja për sisteme me shumë bërthama, faqet e mbështetjes së thellë të kujtesës (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), tabelat e atributeve të faqeve të kujtesës (PAT, Page Attribute Table). Muen gjithashtu ofron një planifikues ciklik të fiksuar mbi bazën e një timer-i që bllokon Intel VMX, një runtime kompakt që nuk ndikon në performancë, një sistem auditimi të dështimeve, një mekanizëm të caktimit statik të burimeve mbi baza rregullash, një sistem për përpunimin e ngjarjeve dhe kanale të kujtesës së ndarë për komunikim brenda komponenteve të ekzekutimit.
Përkrahja e ekzekutimit mbi Muen të komponenteve me kod të makinës 64-bit, 32-bit ose 64-bit makinat virtuale, aplikacione 64-bit në gjuhët Ada dhe SPARK 2014, makinat virtuale me Linux dhe "unikernel" të vetë-mjaftueshëm mbi bazën e MirageOS.
Nova rishtat e propozuara në lëshimin Muen 1.0:
- Dokumentet me specifikimet e bërthamës (struktura dhe arkitektura), sistemin (politikat sistemore, Tau0 dhe mjetet) dhe komponentët janë publikuar, ku dokumentohen të gjitha aspektet e funksionimit të projektit.
- Implementimi i mjeteve Tau0 (Muen System Composer) është shtuar, i cili përfshin një grup komponentësh të verifikuar që janë gati për kompozimin e imazheve sistemore dhe zhvillimin e shërbimeve standarde që ekzekutohen mbi Muen. Ndër komponentët e ofruar janë shoferi AHCI (SATA), Menaxheri i Pajisjeve (DM), bootloaderi, menaxheri sistemik, terminali virtual etj.
- Shoferi Linux muenblock (implementimi i pajisjes bllokuese, i cili punon mbi memorjen e ndarë Muen) është çuar në përdorimin e API blockdev 2.0.
- Janë realizuar mjete për menaxhimin e ciklit të jetës së komponenteve natyrore.
- Imazhet sistemore janë çuar në përdorimin e SBS (Signed Block Stream) dhe CSL (Command Stream Loader) për të mbrojtur integritetin.
- Një shofer i verifikuar AHCI-DRV është realizuar, i shkruar në gjuhën SPARK 2014, duke lejuar lidhjen e pajisjeve që mbështesin interfacin ATA, ose pjesëve të veçanta të disqeve.
- Përkrahja për unikernelin nga projektet MirageOS dhe Solo5 është përmirësuar.
- Mjetet për gjuhën Ada janë përditësuar në lëshimin GNAT Community 2021.
- Sistema i integrimit të vazhdueshëm është çuar nga emulatori Bochs në mjediset e ndërlikuara QEMU/KVM.
- Në imazhet e komponenteve me Linux është përdorur bërthama Linux 5.4.66.
Burimi: opennet.ru
