After eight years of development theproject was , developing the , the absence of errors in the source code of which was confirmed using mathematical methods of formal verification of reliability. The kernel is available for the x86_64 architecture and can be used in mission-critical systems that require an increased level of reliability and guarantee that there are no failures. The source texts of the project are written in the Ada language and its verifiable dialect . The code is under the GPLv3 license.
The partitioning kernel is a microkernel that provides an environment for the execution of components isolated from each other, the interaction of which is tightly regulated by specified rules. Isolation is based on the use ofvirtualization extensions and includes protection mechanisms to block the organization of covert communication channels. The partitioning kernel is more minimalistic and static than other microkernels, which reduces the number of situations that can lead to a failure.
The kernel runs in, similar to a hypervisor, and all other components in non-root VMX mode, similar to guest systems. Hardware access is performed using Intel VT-d DMA extensions and interrupt remapping, which makes it possible to implement secure binding of PCI devices to components running under Muen control.
Muen features support for multi-core systems, nested memory pages (, Extended Page Tables), MSI (Message Signaled Interrupts), memory page attribute tables ( , Page Attribute Table). Muen also provides a fixed loop scheduler based on the Intel VMX preemptive timer, a compact runtime that does not affect performance, a crash auditing system, a rule-based static resource assignment mechanism, an event handling system, and shared memory channels for communication within startup components.
Supports running on top of Muen components with 64-bit native code, 32- or 64-bit virtual machines, 64-bit applications in Ada and SPARK 2014 languages, virtual machines running Linux and self-contained “unikernel” based on.
The main innovations proposed in the Muen 1.0 release are:
- Documents have been published with the specifications of the (device and architecture), (system policies, Tau0 and toolkit) and , which document all aspects of the project.
- The (Muen System Composer) toolkit has been , which includes a set of ready-made verified components for composing system images and developing typical services that run on top of Muen. The provided components include AHCI driver (SATA), Device Manager (DM), bootloader, system manager, virtual terminal, etc.
- The Linux driver (an implementation of a block device that runs on top of Muen shared memory) has been moved to use the blockdev 2.0 API.
- Implemented tools for managing the life cycle of native components.
- System images have been converted to use (Signed Block Stream) and CSL (Command Stream Loader) for integrity protection.
- A verified AHCI-DRV driver written in SPARK 2014 has been implemented, which allows connecting drives that support the ATA interface or separate disk partitions to the components.
- Improved support from and .
- The Hell Language Toolkit has been updated for the GNAT Community 2021 release.
- The continuous integration system was transferred from the Bochs emulator to the nested QEMU / KVM environments.
- The Linux component images use the Linux kernel 5.4.66.