Selepas lapan tahun pembangunan, projek Muen 1.0 telah dikeluarkan, membangunkan kernel Pemisahan, ketiadaan ralat dalam kod sumber yang disahkan menggunakan kaedah matematik pengesahan kebolehpercayaan formal. Kernel tersedia untuk seni bina x86_64 dan boleh digunakan dalam sistem kritikal misi yang memerlukan tahap kebolehpercayaan yang lebih tinggi dan jaminan tiada kegagalan. Kod sumber projek ditulis dalam bahasa Ada dan dialeknya yang boleh disahkan SPARK 2014. Kod itu diedarkan di bawah lesen GPLv3.
Kernel pemisah ialah mikrokernel yang menyediakan persekitaran untuk pelaksanaan komponen yang diasingkan antara satu sama lain, interaksi yang dikawal ketat oleh peraturan yang diberikan. Pengasingan adalah berdasarkan penggunaan sambungan virtualisasi Intel VT-x dan termasuk mekanisme keselamatan untuk menyekat organisasi saluran komunikasi rahsia. Kernel pembahagian adalah lebih minimalis dan statik daripada mikrokernel lain, yang mengurangkan bilangan situasi yang boleh menyebabkan kegagalan.
Kernel berjalan dalam mod akar VMX, serupa dengan hipervisor, dan semua komponen lain berjalan dalam mod bukan akar VMX, serupa dengan sistem tetamu. Akses kepada peralatan dibuat menggunakan sambungan Intel VT-d DMA dan pemetaan semula gangguan, yang memungkinkan untuk melaksanakan pengikatan selamat peranti PCI ke komponen yang dijalankan di bawah Muen.
Keupayaan Muen termasuk sokongan untuk sistem berbilang teras, halaman memori bersarang (EPT, Jadual Halaman Lanjutan), MSI (Sampukan Isyarat Mesej), dan jadual atribut halaman memori (PAT, Jadual Atribut Halaman). Muen juga menyediakan penjadual round-robin tetap berdasarkan pemasa preemptive Intel VMX, masa jalan padat yang tidak menjejaskan prestasi, sistem pengauditan ranap, enjin penetapan sumber statik berasaskan peraturan, sistem pengendalian acara dan saluran memori kongsi untuk komunikasi dalam komponen yang sedang berjalan.
Ia menyokong komponen berjalan dengan kod mesin 64-bit, mesin maya 32- atau 64-bit, aplikasi 64-bit dalam bahasa Ada dan SPARK 2014, mesin maya Linux dan "unikernel" serba lengkap berdasarkan MirageOS di atas Muen.
Inovasi utama yang ditawarkan dalam keluaran Muen 1.0:
- Dokumen telah diterbitkan dengan spesifikasi untuk kernel (peranti dan seni bina), sistem (dasar sistem, Tau0 dan kit alat) dan komponen, yang mendokumenkan semua aspek projek.
- Kit alat Tau0 (Muen System Composer) telah ditambah, yang termasuk satu set komponen disahkan siap sedia untuk mengarang imej sistem dan membangunkan perkhidmatan standard yang berjalan di atas Muen. Komponen yang disediakan termasuk pemacu AHCI (SATA), Pengurus Peranti (DM), pemuat but, pengurus sistem, terminal maya, dsb.
- Pemacu muenblock Linux (pelaksanaan peranti blok yang berjalan di atas memori kongsi Muen) telah ditukar untuk menggunakan API blockdev 2.0.
- Alat yang dilaksanakan untuk mengurus kitaran hayat komponen asli.
- Imej sistem telah ditukar untuk menggunakan SBS (Strim Blok Bertanda) dan CSL (Pemuat Strim Perintah) untuk melindungi integriti.
- Pemacu AHCI-DRV yang disahkan telah dilaksanakan, ditulis dalam bahasa SPARK 2014 dan membolehkan anda menyambung pemacu yang menyokong antara muka ATA atau partition cakera individu kepada komponen.
- Sokongan unikernel yang dipertingkatkan daripada projek MirageOS dan Solo5.
- Kit alat bahasa Ada telah dikemas kini untuk keluaran GNAT Community 2021.
- Sistem penyepaduan berterusan telah dipindahkan daripada emulator Bochs ke persekitaran bersarang QEMU/KVM.
- Imej komponen Linux menggunakan kernel Linux 5.4.66.
Sumber: opennet.ru