After eight years of development, the Muen 1.0 project, which advances the separation kernel, has been released. The absence of errors in the source texts has been 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 a high level of reliability and guaranteed faultlessness. The project's source texts are written in Ada and its verifiable dialect SPARK 2014. The code is distributed under the GPLv3 license.
The separation kernel is a microkernel that provides an environment for executing isolated components, whose interactions are strictly governed by specified rules. The isolation relies on Intel VT-x virtualization extensions and includes mechanisms to block the organization of covert communication channels. The separation kernel is more minimalist and static compared to other microkernels, which helps reduce the number of situations that could lead to failures.
The kernel operates in VMX root mode similar to a hypervisor, while all other components run in VMX non-root mode akin to guest systems. Access to hardware is achieved using Intel VT-d DMA extensions and interrupt remapping, allowing for secure binding of PCI devices to components running under Muen.
Muen supports multicore systems, nested page tables (EPT), Message Signaled Interrupts (MSI), and Page Attribute Tables (PAT). Muen also features a fixed cyclic scheduler based on the preemptive timer from Intel VMX, a compact runtime that does not affect performance, a crash auditing system, a rule-based static resource allocation mechanism, an event handling system, and shared memory channels for interaction within the running components.
It supports running components with 64-bit machine code, 32- or 64-bit applications in Ada and SPARK 2014, Linux virtual machines, and self-contained unikernels based on MirageOS. of virtual machines, 64-разрядных приложений на языках Ada и SPARK 2014, виртуальных машин с Linux и самодостаточных «unikernel» на базе MirageOS.
The main innovations introduced in the Muen 1.0 release:
- Documents have been published with specifications for the kernel (structure and architecture), the system (system policies, Tau0, and tools), and components, documenting all aspects of the project's operation.
- The Tau0 toolset (Muen System Composer) has been added, which includes a set of ready-to-use verified components for composing system images and developing standard services running on top of Muen. Among the provided components are the AHCI (SATA) driver, Device Manager (DM), bootloader, system manager, virtual terminal, and more.
- The Linux driver muenblock (implementation of a block device operating on top of shared memory Muen) has been transitioned to use API blockdev 2.0.
- Tools for managing the lifecycle of native components have been implemented.
- System images have been transitioned to use SBS (Signed Block Stream) and CSL (Command Stream Loader) for integrity protection.
- A verified AHCI-DRV driver, written in SPARK 2014, has been implemented, allowing connection of ATA interface-supporting drives or individual disk partitions to components.
- Support for unikernel from the MirageOS and Solo5 projects has been improved.
- The Ada language toolset has been updated to the GNAT Community 2021 release.
- The continuous integration system has been transitioned from the Bochs emulator to nested QEMU/KVM environments.
- The Linux component images utilize Linux kernel 5.4.66.
Source: opennet.ru
