Pagkatapos ng walong taon ng pag-unlad, ang Muen 1.0 na proyekto ay inilabas, na binuo ang Separation kernel, ang kawalan ng mga error sa source code na kung saan ay nakumpirma gamit ang mga pamamaraan ng matematika ng pormal na pag-verify ng pagiging maaasahan. Ang kernel ay magagamit para sa x86_64 architecture at maaaring gamitin sa mission-critical system na nangangailangan ng mas mataas na antas ng pagiging maaasahan at garantiya ng walang mga pagkabigo. Ang source code ng proyekto ay nakasulat sa wikang Ada at ang nabe-verify na dialect nito na SPARK 2014. Ang code ay ipinamamahagi sa ilalim ng lisensya ng GPLv3.
Ang separation kernel ay isang microkernel na nagbibigay ng isang kapaligiran para sa pagpapatupad ng mga bahagi na nakahiwalay sa isa't isa, ang pakikipag-ugnayan nito ay mahigpit na kinokontrol ng ibinigay na mga patakaran. Nakabatay ang paghihiwalay sa paggamit ng mga extension ng virtualization ng Intel VT-x at kasama ang mga mekanismo ng seguridad upang harangan ang organisasyon ng mga patagong channel ng komunikasyon. Ang partitioning kernel ay mas minimalistic at static kaysa sa iba pang microkernels, na binabawasan ang bilang ng mga sitwasyon na maaaring magdulot ng pagkabigo.
Ang kernel ay tumatakbo sa VMX root mode, katulad ng isang hypervisor, at lahat ng iba pang bahagi ay tumatakbo sa VMX non-root mode, katulad ng mga guest system. Ginagawa ang access sa kagamitan gamit ang mga extension ng Intel VT-d DMA at interrupt remapping, na ginagawang posible na ipatupad ang secure na pag-binding ng mga PCI device sa mga bahaging tumatakbo sa ilalim ng Muen.
Kasama sa mga kakayahan ni Muen ang suporta para sa mga multi-core system, mga nested memory page (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), at memory page attribute table (PAT, Page Attribute Table). Nagbibigay din ang Muen ng fixed round-robin scheduler batay sa Intel VMX preemptive timer, isang compact runtime na hindi nakakaapekto sa performance, isang crash auditing system, isang rule-based na static resource assignment engine, isang event handling system, at shared memory channel para sa komunikasyon sa loob ng tumatakbong mga bahagi.
Sinusuportahan nito ang mga tumatakbong bahagi na may 64-bit machine code, 32- o 64-bit na virtual machine, 64-bit na application sa Ada at SPARK 2014 na wika, Linux virtual machine at self-contained na "unikernels" batay sa MirageOS sa ibabaw ng Muen.
Ang mga pangunahing inobasyon na inaalok sa paglabas ng Muen 1.0:
- Ang mga dokumento ay nai-publish na may mga detalye para sa kernel (device at architecture), system (system policy, Tau0 at toolkit) at mga bahagi, na nagdodokumento sa lahat ng aspeto ng proyekto.
- Ang Tau0 (Muen System Composer) toolkit ay idinagdag, na kinabibilangan ng isang set ng mga nakahanda nang na-verify na bahagi para sa pagbuo ng mga imahe ng system at pagbuo ng mga karaniwang serbisyo na tumatakbo sa ibabaw ng Muen. Ang mga bahaging ibinigay ay kinabibilangan ng AHCI driver (SATA), Device Manager (DM), boot loader, system manager, virtual terminal, atbp.
- Ang driver ng muenblock Linux (isang pagpapatupad ng block device na tumatakbo sa ibabaw ng nakabahaging memorya ng Muen) ay na-convert upang gamitin ang blockdev 2.0 API.
- Mga ipinatupad na tool para sa pamamahala sa ikot ng buhay ng mga katutubong bahagi.
- Ang mga imahe ng system ay na-convert upang gamitin ang SBS (Signed Block Stream) at CSL (Command Stream Loader) upang protektahan ang integridad.
- Naipatupad ang isang na-verify na driver ng AHCI-DRV, na nakasulat sa wikang SPARK 2014 at nagbibigay-daan sa iyong ikonekta ang mga drive na sumusuporta sa interface ng ATA o indibidwal na mga partisyon ng disk sa mga bahagi.
- Pinahusay na suporta sa unikernel mula sa mga proyekto ng MirageOS at Solo5.
- Ang toolkit ng wikang Ada ay na-update para sa paglabas ng GNAT Community 2021.
- Ang tuluy-tuloy na sistema ng pagsasama ay inilipat mula sa Bochs emulator sa QEMU/KVM nested environment.
- Gumagamit ng Linux 5.4.66 kernel ang mga component ng Linux.
Pinagmulan: opennet.ru