After eight years of development, the Muen 1.0 project was released, developing the Separation kernel, the absence of errors in the source code of which was confirmed using mathematical methods of formal reliability verification. 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 a guarantee that there will be no failures. The source texts of the project are written in the Ada language and its verifiable SPARK 2014 dialect. The code is distributed under the GPLv3 license.
The separation kernel is a microkernel that provides an environment for the execution of components isolated from each other, the interaction of which is strictly regulated by specified rules. Isolation is based on the use of Intel VT-x virtualization 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 crash.
The kernel runs in root VMX mode, similar to the hypervisor, and all other components run 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 securely bind PCI devices to components running under Muen.
Of the capabilities of Muen, support for multi-core systems, nested memory pages (EPT, Extended Page Tables), MSI (Message Signaled Interrupts), memory page attribute tables (PAT, Page Attribute Table) is noted. Muen also provides a fixed loop scheduler based on the preemptive Intel VMX 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 running components.
It supports running 64-bit native components, 32-bit or 64-bit virtual machines, 64-bit Ada and SPARK 2014 applications, Linux virtual machines, and MirageOS-based self-contained unikernels on top of Muen.
The main innovations proposed in the release of Muen 1.0:
- Kernel (device and architecture), system (system policies, Tau0 and toolkit) and component specification documents have been published, documenting all aspects of the project.
- The Tau0 (Muen System Composer) toolkit has been added, which includes a set of ready-made verified components for compiling system images and developing typical services that run on top of Muen. Components provided include AHCI driver (SATA), Device Manager (DM), boot loader, system manager, virtual terminal, etc.
- The muenblock Linux driver (an implementation of a block device running on top of Muen shared memory) has been migrated to use the blockdev 2.0 API.
- Implemented tools for managing the life cycle of native components.
- System images have been migrated to use SBS (Signed Block Stream) and CSL (Command Stream Loader) for integrity protection.
- A verified AHCI-DRV driver has been implemented, written in the SPARK 2014 language and allowing you to connect drives that support the ATA interface or separate disk partitions to the components.
- Improved unikernel support from MirageOS and Solo5 projects.
- The Ada language toolkit has been updated for the GNAT Community 2021 release.
- The continuous integration system has been transferred from the Bochs emulator to QEMU/KVM nested environments.
- The Linux component images use the Linux 5.4.66 kernel.
Source: opennet.ru