Sawise wolung taun pembangunan, proyek Muen 1.0 dirilis, ngembangake kernel Separation, ora ana kesalahan ing kode sumber sing dikonfirmasi nggunakake metode matematika verifikasi keandalan formal. Kernel kasedhiya kanggo arsitektur x86_64 lan bisa digunakake ing sistem kritis misi sing mbutuhake tingkat linuwih lan njamin ora gagal. Kode sumber proyek kasebut ditulis nganggo basa Ada lan dialek sing bisa diverifikasi SPARK 2014. Kode kasebut disebarake miturut lisensi GPLv3.
Kernel pemisahan yaiku mikrokernel sing nyedhiyakake lingkungan kanggo eksekusi komponen sing diisolasi saka siji liyane, interaksi sing diatur kanthi ketat dening aturan sing diwenehake. Isolasi adhedhasar panggunaan ekstensi virtualisasi Intel VT-x lan kalebu mekanisme keamanan kanggo mblokir organisasi saluran komunikasi rahasia. Kernel pemisahan luwih minimalis lan statis tinimbang mikrokernel liyane, sing nyuda jumlah kahanan sing bisa nyebabake kegagalan.
Kernel mlaku ing mode root VMX, padha karo hypervisor, lan kabeh komponen liyane mlaku ing mode non-root VMX, padha karo sistem tamu. Akses menyang peralatan digawe nggunakake ekstensi DMA Intel VT-d lan ngganggu remapping, kang ndadekake iku bisa kanggo ngleksanakake naleni aman saka piranti PCI kanggo komponen mlaku ing Muen.
Kapabilitas Muen kalebu dhukungan kanggo sistem multi-inti, kaca memori nested (EPT, Tabel Kaca Extended), MSI (Pesen Signaled Interrupts), lan tabel atribut kaca memori (PAT, Tabel Atribut Kaca). Muen uga nyedhiyakake panjadwal round-robin tetep adhedhasar timer preemptive Intel VMX, runtime kompak sing ora mengaruhi kinerja, sistem audit kacilakan, mesin penugasan sumber daya statis adhedhasar aturan, sistem penanganan acara, lan saluran memori bareng kanggo komunikasi ing komponen mlaku.
Ndhukung komponen mlaku karo kode mesin 64-dicokot, 32- utawa 64-dicokot mesin virtual, aplikasi 64-dicokot ing Ada lan SPARK 2014 basa, mesin virtual Linux lan poto-sing "unikernels" adhedhasar MirageOS ing ndhuwur Muen.
Inovasi utama sing ditawakake ing release Muen 1.0:
- Dokumen wis diterbitake kanthi spesifikasi kanggo kernel (piranti lan arsitektur), sistem (kabijakan sistem, Tau0 lan toolkit) lan komponen, sing nyathet kabeh aspek proyek kasebut.
- Tau0 (Muen System Composer) toolkit wis ditambahakΓ©, kang kalebu pesawat saka siap-digawe komponen diverifikasi kanggo gambar sistem nyusun lan ngembangaken layanan standar sing mbukak ing ndhuwur Muen. Komponen sing diwenehake kalebu driver AHCI (SATA), Device Manager (DM), boot loader, manajer sistem, terminal virtual, lsp.
- Pembalap muenblock Linux (implementasine piranti pemblokiran sing mlaku ing ndhuwur memori bareng Muen) wis diowahi kanggo nggunakake API blockdev 2.0.
- Piranti sing ditrapake kanggo ngatur siklus urip komponen asli.
- Gambar sistem wis diowahi kanggo nggunakake SBS (Signed Block Stream) lan CSL (Command Stream Loader) kanggo nglindhungi integritas.
- Driver AHCI-DRV sing wis diverifikasi wis dileksanakake, ditulis ing basa SPARK 2014 lan ngidini sampeyan nyambungake drive sing ndhukung antarmuka ATA utawa partisi disk individu menyang komponen.
- Dhukungan unikernel sing luwih apik saka proyek MirageOS lan Solo5.
- Toolkit basa Ada wis dianyari kanggo rilis Komunitas GNAT 2021.
- Sistem integrasi terus-terusan wis ditransfer saka emulator Bochs menyang lingkungan bersarang QEMU / KVM.
- Gambar komponen Linux nggunakake kernel Linux 5.4.66.
Source: opennet.ru