Saatos dalapan taun pangwangunan, proyék Muen 1.0 dileupaskeun, ngembangkeun kernel Separation, henteuna kasalahan dina kode sumber anu dikonfirmasi ngagunakeun métode matematis verifikasi reliabilitas formal. Kernel sayogi pikeun arsitéktur x86_64 sareng tiasa dianggo dina sistem kritis-misi anu meryogikeun tingkat réliabilitas sareng jaminan henteu aya kagagalan. Kodeu sumber proyék ditulis dina basa Ada sareng dialék anu tiasa diverifikasi SPARK 2014. Kodeu disebarkeun dina lisénsi GPLv3.
Kernel separation mangrupikeun mikrokernel anu nyayogikeun lingkungan pikeun palaksanaan komponén anu terasing tina silih, interaksina diatur sacara ketat ku aturan anu dipasihkeun. Isolasi didasarkeun kana panggunaan ekstensi virtualisasi Intel VT-x sareng kalebet mékanisme kaamanan pikeun meungpeuk organisasi saluran komunikasi rahasia. Kernel partisi langkung minimalis sareng statik tibatan mikrokernel anu sanés, anu ngirangan jumlah kaayaan anu tiasa nyababkeun gagalna.
Kernel dijalankeun dina modeu root VMX, mirip sareng hypervisor, sareng sadaya komponén sanésna dijalankeun dina modeu non-root VMX, sami sareng sistem tamu. Aksés ka alat-alat dijieun maké Intel VT-d DMA ekstensi sarta ngaganggu remapping, nu ngamungkinkeun pikeun nerapkeun beungkeutan aman alat PCI kana komponén ngajalankeun handapeun Muen.
Kamampuhan Muen kalebet dukungan pikeun sistem multi-inti, halaman mémori bersarang (EPT, Tabel Halaman Dipanjangkeun), MSI (Pesen Signaled Interrupts), sareng tabel atribut halaman mémori (PAT, Tabel Atribut Halaman). Muen ogé nyayogikeun penjadwalan round-robin tetep dumasar kana timer preemptive Intel VMX, waktos jalan kompak anu henteu mangaruhan kinerja, sistem audit kacilakaan, mékanisme ngerjakeun sumber daya statik dumasar aturan, sistem penanganan acara, sareng saluran mémori anu dibagikeun pikeun komunikasi dina komponén ngajalankeun.
Ieu ngarojong ngajalankeun komponén kalawan kode mesin 64-bit, 32- atawa 64-bit mesin virtual, aplikasi 64-bit dina basa Ada na SPARK 2014, mesin virtual Linux Ubuntu jeung timer ngandung "unikernels" dumasar kana MirageOS on luhureun Muen.
Inovasi utama anu ditawarkeun dina sékrési Muen 1.0:
- Dokumén parantos diterbitkeun kalayan spésifikasi pikeun kernel (alat sareng arsitéktur), sistem (kawijakan sistem, Tau0 sareng toolkit) sareng komponén, anu ngadokumentasikeun sadaya aspek proyék.
- Tau0 (Muen System Composer) toolkit geus ditambahkeun, nu ngawengku susunan siap-dijieun komponén diverifikasi pikeun nyusun gambar sistem jeung ngamekarkeun jasa baku nu ngajalankeun on luhureun Muen. Komponén anu disayogikeun kalebet supir AHCI (SATA), Manajer Alat (DM), boot loader, manajer sistem, terminal virtual, jsb.
- Supir muenblock Linux Ubuntu (hiji palaksanaan hiji alat block ngajalankeun on luhureun memori dibagikeun Muen) geus dirobah jadi make blockdev 2.0 API.
- Alat anu dilaksanakeun pikeun ngatur siklus kahirupan komponén asli.
- Gambar sistem geus dirobah ngagunakeun SBS (Signed Block Stream) jeung CSL (Command Stream Loader) pikeun ngajaga integritas.
- Supir AHCI-DRV anu diverifikasi parantos dilaksanakeun, ditulis dina basa SPARK 2014 sareng ngamungkinkeun anjeun nyambungkeun drive anu ngadukung antarmuka ATA atanapi partisi disk individu kana komponén.
- Ningkatkeun dukungan unikernel tina proyék MirageOS sareng Solo5.
- Alat basa Ada parantos diropéa kanggo GNAT Community 2021 release.
- Sistem integrasi kontinyu geus ditransfer ti émulator Bochs ka QEMU / lingkungan nested KVM.
- Gambar komponén Linux nganggo kernel Linux 5.4.66.
sumber: opennet.ru