Muen 1.0 released, an open source microkernel for building highly reliable systems

Share on Facebook Share on Twitter Pinterest LinkedIn Tumblr

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 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 SPARK 2014 . The code is distributed 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 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 failure.

The kernel runs in VMX root mode , 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 1.0 released, an open source microkernel for building highly reliable systems

Muen features support for multi-core systems, nested memory pages ( EPT , Extended Page Tables), MSI (Message Signaled Interrupts), memory page attribute tables ( PAT , 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.

MX Linux 21 is uploaded to Debian 11 to offer its most refined version to date

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 MirageOS .

The main innovations proposed in the Muen 1.0 release are:

  • Documents have been published with the specifications of the kernel (device and architecture), systems (system policies, Tau0 and toolkit) and components , which document all aspects of the project.
  • The Tau0 (Muen System Composer) toolkit has been added , 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 muenblock 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 SBS (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 unikernel support from MirageOS and Solo5 projects.
  • 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.

Write A Comment