[ANN] Muen version 1.0 released

[Reto Buerki]

Hi,

More than eight years of continued development after the initial
publication, we are proud to announce the 1.0 release of the Muen
Separation Kernel (SK).

The news that excites us the most is that Muen was selected by several
vendors as the foundation for their security products. Most notably, it
is employed by secunet as the platform for their Communicator H product
[1], which has been certified up to "GEHEIM" by the German BSI [2].
Furthermore, Muen was also chosen for Nitrokey's NetHSM product [3].

Besides many small improvements and fixes in various areas of the
project, the most prominent features in this 1.0 release are:

- Availability of the Muen System Specification document [4]
- Availability of the Muen Kernel Specification document [5]
- Availability of the Muen Component Specification document [6]
- Add trusted τ0 System Resource Manager [7]
- Implement native AHCI driver component in SPARK 2014
- Update Linux muenblock driver to blockdev 2.0 API
- Implement native component life-cycle management
- Switch to SBS/CSL [8] system images
- Improve support for MirageOS/Solo5 unikernels
- Upgrade to GNAT Community 2021 toolchain
- CI: Switch from Bochs to nested QEMU/KVM
- Update VM guest Linux kernel to v5.4.66

For the interested reader, the following sections provide further
details on the features listed above.

Specification Documents
-----------------------

Muen now provides comprehensive documentation for all aspects of the
project:

System Specification
~~~~~~~~~~~~~~~~~~~~
The System Specification document [4] explains the Muen system policy,
the τ0 concept and the toolchain.

It also specifies and explains the XML schema used to declare a Muen system.

Kernel Specification
~~~~~~~~~~~~~~~~~~~~
The Kernel Specification document [5] gives an overview of the Muen
kernel design and architecture. It then specifies the data model and
outlines the implementation.

Component Specification
~~~~~~~~~~~~~~~~~~~~~~~
The Component Specification document [6] is intended for developers and
integrators of native as well as VM components. After the introduction
where the component concept of Muen is explained, the document specifies
the resource discovery mechanism, vCPU profiles, subject
monitoring/lifecycle management and the interfaces provided by the Muen
platform.

τ0 System Resource Manager
--------------------------

For an introduction to the Tau0 (τ0) concept, see chapter 4 in [4].

In this release, the static variant has been implemented, where τ0 is
used as trusted system image composer, which replaces the mupack-based
toolchain, more specifically the following tools:

- mugeniobm
- mugenmsrbm
- mugenvtd
- mugenpt
- mupack

τ0 accepts a command stream, i.e. a stream of instructions that describe
how to modify the system image state. Each command is checked for
validity and against the system invariants. It is executed only if the
checks are successful, so that each performed command leads again to a
sound system image state.

For more details about τ0, see also its website [7].

Native AHCI Driver
------------------

The AHCI-DRV is a native driver for SATA devices connected to a
AHCI-Port. It is implemented in SPARK 2014 with proof of absence of
runtime errors. The driver supports basic ATA-Commands such as

- read & write
- discard
- sync
- get-S.M.A.R.T.

The included server can be configured in different ways to connect to
native components as well as muenblock Linux devices. As GPT Parsing is
also implemented it is possible to attach only partitions to server
ports rather than exporting the whole device.

The existing muenblock [9] device driver has been updated to version 2.0
of the blockdev interface. This interface allows zero copy operation and
brings much improved performance.

Native Component Life-cycle Management
--------------------------------------

It is now possible to init/restart native components in a controlled
manner. The mechanism of Lifecycle management is described in detail in
[6], chapter 6.

SBS/CSL
-------

This release drops support for Multiboot images and adds support for an
implementation of the "Bootloader Signed Block Stream of Commands"
(BSBSC) concept. The motivation, protocol specifications and links to
the reference implementation is described in [8].

MirageOS/Solo5 Unikernels
-------------------------

This release seamlessly integrates the Solo5 manifest/multi-device
support with Muen, making MirageOS/Solo5 a first class citizen of the
eco system.

Also, the project website https://muen.sk is served by a MirageOS/Solo5
unikernel running on Muen. The details how this is done exactly is
explained in the articles [10],[11].

CI: Switch to QEMU/KVM (nested)
-------------------------------

The CI system has been switched from the Bochs emulator to nested
QEMU/KVM. This has the advantage that QEMU/KVM can provide a fully
featured virtualized system, including IOMMU and virtio-based devices.
It also brings a great speed up for CI.

Switching to QEMU/KVM also allowed us to add a system booting via
coreboot->FILO->SBS->CSL->Muen to CI testing.

Please feel free to give the latest version of Muen a try. As always,
feedback is very much appreciated!

Kind regards,
The Muen Team

[1] - https://www.secunet.com/loesungen/sina-communicator-h
[2] -
https://www.bsi.bund.de/DE/Themen/Oeffentliche-Verwaltung/Zulassung/Liste-zugelassener-Produkte/liste-zugelassener-produkte_node.html
[3] - https://www.nitrokey.com/products/nethsm
[4] - https://muen.sk/muen-system-spec.pdf
[5] - https://muen.sk/muen-kernel-spec.pdf
[6] - https://muen.sk/muen-component-spec.pdf
[7] - https://muen.sk/tau0.html
[8] - https://muen.sk/bsbsc-spec.pdf
[9] - https://git.codelabs.ch/?p=muen/linux/muenblock.git
[10] - https://muen.sk/articles.html#mirageos-unikernels
[11] - https://muen.sk/articles.html#the-muen-sk-website