Pas pas tetë vite zhvillimi, projekti Muen 1.0, i cili zhvillon kernelin e ndarjes (Separation kernel), doli në dritë, pa asnjë gabim në kodin burimor, të konfirmuar përmes metodave matematikore të vërtetimit formal të besueshmërisë. Kernel-i është i disponueshëm për arkitekturën x86_64 dhe mund të përdoret në sisteme kritike që kërkojnë një nivel të lartë të besueshmërisë dhe garanci për mungesën e çrregullsive. Kodet burimore të projektit janë shkruar në gjuhën Ada dhe në dialektin e saj të verifikueshëm SPARK 2014. Kodi shpërndahet sipas licencës GPLv3.
Kernel-i i ndarjes paraqet një mikrokernel që ofron një mjedis për përfitimin e komponenteve të izoluara nga njëra-tjetra, ndërveprimi i të cilave rregullohet rreptësisht nga rregulla të caktuara. Izolimi bazohet në përdorimin e zgjerimeve të virtualizimit Intel VT-x dhe përfshin mekanizma mbrojtëse 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, gjë që lejon të reduktojë numrin e situatave që mund të çojnë në çrregullim.
Kernel-i funksionon në modin rrënjësor VMX, ngjashëm me hipervizorin, ndërsa të gjitha komponentët e tjerë në modin jo-rrënjësor VMX, ngjashëm me sistemet mysafire. Qasja në pajisje realizohet me përdorimin e zgjerimeve Intel VT-d DMA dhe rimapping të ndërprerjeve, që lejon implementimin e lidhjes së sigurt të pajisjeve PCI me komponentët e drejtuar nga Muen.
Nga mundësitë e Muen, përmendet mbështetje për sisteme me shumë bërthama, faqe të brendshme të memories (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), tabela të atributit të faqeve të memories (PAT, Page Attribute Table). Muen gjithashtu ofron një planifikues ciklik të palëkundur të bazuar në qullin e zëvendësimit Intel VMX, një runtime kompak që nuk ndikon në performancë, një sistem auditi të dështimeve, një mekanizëm për caktimin statik të burimeve mbi baza rregullash, një sistem për përpunimin e ngjarjeve dhe kanale të memories së ndarë për ndërveprimin brenda komponentëve të aktivizuar.
MbĂ«shtetet ekzekutimi mbi Muen tĂ« komponentĂ«ve me kod makinor 64-bit, 32- ose 64-bit makinave virtuale, aplikacione 64-bit nĂ« gjuhĂ«t Ada dhe SPARK 2014, makina virtuale me Linux dhe âunikernelâ tĂ« pavarura mbi MirageOS.
Risi kryesore të ofruara në lëshimin e Muen 1.0:
- Dokumentet me specifikimet e kernel-it (struktura dhe arkitektura), sistemin (politikat sistemore, Tau0 dhe mjetet) dhe komponentët janë publikuar, në të cilat janë dokumentuar të gjitha aspektet e funksionimit të projektit.
- I është shtuar mjeti Tau0 (Muen System Composer), i cili përfshin një grup të komponentëve të verifikuar për përbërjen e imazheve sistemore dhe zhvillimin e shërbimeve tipike, të cilat ekzekutohen mbi Muen. Ndër komponentët e ofruara janë: drejtori AHCI (SATA), Menaxheri i Pajisjeve (DM), bootloader, menaxheri sistemor, terminal virtual etj.
- Drejtori Linux muenblock (implementimi i pajisjeve bllokuese që funksionon mbi memorien e ndarë Muen) është aktualizuar për të përdorur API blockdev 2.0.
- Janë realizuar mjete për menaxhimin e ciklit të jetës së komponentëve natyrorë.
- Imazhet sistemore janë përditësuar për të përdorur SBS (Signed Block Stream) dhe CSL (Command Stream Loader) për të mbrojtur integritetin.
- Një drejtori i verifikuar AHCI-DRV, i shkruar në gjuhën SPARK 2014, është realizuar, i cili lejon lidhjen e magazinave që mbështesin ndërfaqen ATA, ose pjesët e veçanta të disqeve me komponentët.
- Mbështetje e përmirësuar për unikernel nga projektet MirageOS dhe Solo5.
- Mjetet për gjuhën Ada janë përditësuar në versionin GNAT Community 2021.
- Sistemi i integrimit të vazhdueshëm është kaluar nga simulatori Bochs në ambientet e brendshme QEMU/KVM.
- Në imazhet e komponentëve me Linux është përdorur bërthama Linux 5.4.66.
Burimi: opennet.ru
