Setelah delapan tahun pengembangan, proyek Muen 1.0 dirilis, mengembangkan kernel Separation, tidak adanya kesalahan dalam kode sumber yang dikonfirmasi menggunakan metode matematis untuk verifikasi keandalan formal. Kernel tersedia untuk arsitektur x86_64 dan dapat digunakan dalam sistem kritis yang memerlukan peningkatan tingkat keandalan dan jaminan tidak ada kegagalan. Kode sumber proyek ini ditulis dalam bahasa Ada dan dialeknya yang dapat diverifikasi SPARK 2014. Kode ini didistribusikan di bawah lisensi GPLv3.
Kernel pemisahan adalah mikrokernel yang menyediakan lingkungan untuk eksekusi komponen yang terisolasi satu sama lain, yang interaksinya diatur secara ketat oleh aturan yang diberikan. Isolasi didasarkan pada penggunaan ekstensi virtualisasi Intel VT-x dan mencakup mekanisme keamanan untuk memblokir organisasi saluran komunikasi rahasia. Kernel yang dipartisi lebih minimalis dan statis dibandingkan mikrokernel lainnya, sehingga mengurangi jumlah situasi yang dapat menyebabkan kegagalan.
Kernel berjalan dalam mode root VMX, mirip dengan hypervisor, dan semua komponen lainnya berjalan dalam mode non-root VMX, mirip dengan sistem tamu. Akses ke peralatan dilakukan menggunakan ekstensi Intel VT-d DMA dan pemetaan ulang interupsi, yang memungkinkan penerapan pengikatan aman perangkat PCI ke komponen yang berjalan di bawah Muen.
Kemampuan Muen mencakup dukungan untuk sistem multi-core, halaman memori bersarang (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), dan tabel atribut halaman memori (PAT, Page Attribute Table). Muen juga menyediakan penjadwal round-robin tetap berdasarkan pengatur waktu preemptive Intel VMX, runtime ringkas yang tidak memengaruhi kinerja, sistem audit kerusakan, mekanisme penetapan sumber daya statis berbasis aturan, sistem penanganan peristiwa, dan saluran memori bersama untuk komunikasi dalam komponen yang sedang berjalan.
Ini mendukung komponen yang berjalan dengan kode mesin 64-bit, mesin virtual 32 atau 64-bit, aplikasi 64-bit dalam bahasa Ada dan SPARK 2014, mesin virtual Linux dan “unikernel” mandiri berdasarkan MirageOS di atas Muen.
Inovasi utama yang ditawarkan pada rilis Muen 1.0:
- Dokumen telah diterbitkan dengan spesifikasi untuk kernel (perangkat dan arsitektur), sistem (kebijakan sistem, Tau0 dan toolkit) dan komponen, yang mendokumentasikan semua aspek proyek.
- Toolkit Tau0 (Muen System Composer) telah ditambahkan, yang mencakup serangkaian komponen terverifikasi siap pakai untuk menyusun gambar sistem dan mengembangkan layanan standar yang berjalan di atas Muen. Komponen yang disediakan antara lain driver AHCI (SATA), Device Manager (DM), boot loader, system manager, virtual terminal, dll.
- Driver muenblock Linux (implementasi perangkat blok yang berjalan di atas memori bersama Muen) telah dikonversi untuk menggunakan API blockdev 2.0.
- Alat yang diterapkan untuk mengelola siklus hidup komponen asli.
- Gambar sistem telah dikonversi untuk menggunakan SBS (Signed Block Stream) dan CSL (Command Stream Loader) untuk melindungi integritas.
- Driver AHCI-DRV terverifikasi telah diterapkan, ditulis dalam bahasa SPARK 2014 dan memungkinkan Anda menghubungkan drive yang mendukung antarmuka ATA atau partisi disk individual ke komponen.
- Peningkatan dukungan unikernel dari proyek MirageOS dan Solo5.
- Toolkit bahasa Ada telah diperbarui untuk rilis Komunitas GNAT 2021.
- Sistem integrasi berkelanjutan telah ditransfer dari emulator Bochs ke lingkungan bersarang QEMU/KVM.
- Gambar komponen Linux menggunakan kernel Linux 5.4.66.
Sumber: opennet.ru