[ANN] Muen version 1.1 released

[Adrian-Ken Rueegsegger]

Hello,

After a long period of active development (the last release was two
years ago), we are delighted to announce the release of the Muen
Separation Kernel (SK) v1.1.

Aside a plethora of various minor fixes and improvements all around the
project, the following sections list the most prominent changes.

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

Kind regards,
The Muen Team


## Documentation
The different Muen specification documents [1] have been updated to
include descriptions of all the enhancements and changes. The new set of
docs now have the version number v0.7.2 and they should touch on all
important topics.

Additionally, the Debug Server component gained it's own Documentation
which lives alongside the source code under components/dbgserver/README.md.

## Implement support for scheduling partitions
Since Muen employs static scheduling, in more advanced scenarios where a
system consists of a large number of subjects, the generation and
management of static scheduling plans can become rather time consuming
and complex. Support of scheduling partitions can therefore greatly
reduce the number of scheduling plans.

While scheduling groups support the efficient cooperation of multiple
subjects, subjects which need to be spatially but not temporally
isolated from each other cannot profit from it.

The addition of scheduling partitions supplements scheduling groups. The
scheduling plan schedules scheduling partitions consisting of scheduling
groups consisting of subjects. Prior scheduling behavior is equivalent
to all scheduling partitions having exactly one scheduling group.

Within a scheduling partition, all scheduling groups are scheduled round
robin with preemption and the opportunity to yield and/or sleep. A
prioritization is not implemented on purpose to avoid any starvation issues.

Please refer to the updated Muen Kernel Specification documentation for
further information regarding the scheduler.

Subjects can trigger source events with a yield action if they want to
relinquish the remainder of the minor frame to a different scheduling
group in the same partition. This instructs the kernel to reschedule the
scheduling partition, i.e. look for the next runnable scheduling group
and schedule the current subject of that group. If there is no other
runnable group, the same subject will be scheduled again.

For sleep events, the subject is marked as not running and the same
actions are performed as for yield. If no other group is runnable then
the scheduling partition itself is put in a sleep state.

Sleeping subjects are woken up whenever an event or interrupt is pending
or when the associated subject timed event expires.

Please refer to the updated Muen Component Specification documentation
for further information on subject yield and sleep.

As a consequence of these enhancements and the extended policy XML
format for scheduling plans, the Mugenschedcfg tool has been deprecated
and removed. Please refer to the update Muen System Specification
documentation for more details on the new scheduling plan XML format.

## Support for CPU microcode updates (MCU)
The Muen kernel has been extended to apply CPU microcode updates during
startup of the system, when an applicable MCU file has been provided in
the system policy.

The new Mucfgucode tool, which leverages the iucode-tool [2] behind the
scenes, automates the addition of a physical memory region containing
the MCU file to the policy. It can be configured via the following
environment variables:

### MUEN_UCODE_DIR
Directory containing the Intel microcode files (e.g.
/lib/firmware/intel-ucode)

### MUEN_IUCODE_TOOL_PATH
Path to the iucode-tool (default: /usr/sbin)

Note that an update region is only added to the policy if an MCU
applicable for the CPU of the hardware specified in the policy is found.

## Enable subjects to use XSAVE feature
The FPU-related XCR0 register is now managed on a per-subject basis and
subjects can use the `xsetbv` instruction to change its value. Via the
revamped CPUID emulation code, the SM subject (conditionally) announces
the availability of XSAVE features, which enables Linux subjects to use
more advanced features of the FPU.

## Enable assignment of Thermal/Power/Energy-related MSRs
This allows system integrators to assign Model-Specific Registers (MSRs)
related to Power- and Energy management to subjects. The newly
whitelisted MSRs include:

- `MSR_PLATFORM_INFO`
- `IA32_THERM_STATUS`
- `IA32_TEMPERATURE_TARGET`
- `IA32_PACKAGE_THERM_STATUS`
- `MSR_RAPL_POWER_UNIT`
- `MSR_PKG_POWER_LIMIT`
- `MSR_PKG_ENERGY_STATUS`
- `MSR_DRAM_ENERGY_STATUS`
- `MSR_PP1_ENERGY_STATUS`
- `MSR_CONFIG_TDP_CONTROL`
- `IA32_PM_ENABLE`
- `IA32_HWP_CAPABILITIES`
- `IA32_HWP_REQUEST`

Note that since a lot of information and capabilities are enabled via
these MSRs, the policy writer must carefully consider the security
ramifications of granting subjects access to these registers.

## Hardware Support
Version 1.1.0 of Muen has been verified to run on systems with an Intel
12th generation Alder Lake CPU.

## Policy and Toolchain
Numerous improvements and fixes have been applied to the toolchain. It
has also been optimized to significantly boost the speed when processing
large XML system policies.

Furthermore, Tau0 static has been extended to enable skipping of hash
verification during development. This feature is controlled via the
`TAU0_SKIP_HASHING` environment variable.

### Switch from Community 2021 to GNAT FSF 12.2 toolchain
The toolchain used for compilation and verification of the Muen project
source code has been switched to the one provided by Alire [3], the Ada
Library repository.

### Introduction of XML templates and amend mechanism
The purpose of templates and amend-statements is to avoid duplication in
the XML policy and make the configuration files more readable by
providing a way to insert XML blocks at particular places. The
templating and the amend concepts are independent from each other.
Templates can define building blocks and help to provide a high-level
view of a system.

When two building blocks are connected via a channel or when a subject
behaves like a client of another subject, it is desirable to insert a
communication channel into a subject from “outside” of that subject.
Such additions to an XML node are now possible with amend statements. On
evaluation, the children of an amend-node are merged into the children
of the node specified by the given XPath.

### Implement virtual resource allocation
To alleviate the need for policy writers to manually place all virtual
memory regions and channels as well as assign numbers to logical events
and vectors, two new tools called `mucfgcvresalloc` and `mucfgvresalloc`
are provided. They implement automated allocation of the following
virtual resources:

- `virtualAddress` for memory regions and channels
- `event` and `vector` numbers for channels

The `mucfgcvresalloc` tool provides autoallocation of virtual resources
in the component XML specification. In addition to the above listed
attributes, it also handles `virtualAddressBase`, `eventBase` and
`vectorBase` of memory and channel arrays.

Analogously, the `mucfgvresalloc` provides autoallocation of virtual
resources for subjects in the source policy.

To request autoallocation for a `virtualAddress`, simply omit the
attribute. To request autoallocation for `event` or `vector`, set the
respective attribute to `auto`.

Note that some virtual resources cannot be autoallocated. In particular
all resources in libraries and those associated with devices.

### Introduce Toolchain Plugins
The intention of the new plugin system for XML policy processing is to
simplify the introduction of small, less critical modifications to the
toolchain and keep those extensions separate from the *core* Muen toolchain.

An example for such a use case is the documentation plugin. It can be
employed to build documentation for a system from a single information
source (the XML policy), with the user being in a position to easily
adjust the functionality and the underlying XSD schema. To remove the
additional information from the policy, the `muxmlfilter` tool is
provided. It strips the extra elements that are not part of the core XML
policy format, so it can be processed by tools that are oblivious of the
additional information.

For further information, refer to the Muen System Specification
documentation, in particular sections *5.2 Plugin System* and *5.4 Plugins*.

### Improve loader expansion and Zero-Page initramfs handling
Loader expansion has been reworked in order for Loader subjects to keep
sharing the source region if the same, file-backed region has been
mapped by multiple subjects under loader control. This removes data
duplication and can significantly reduce the system image size.

Furthermore, writable initrd regions are now marked as RAM in generated
Linux Zero Page structures. This lets Linux reclaim/-use these initrd
memory regions after boot. Otherwise the chunk of memory remains unused
for the lifetime of the Linux subject. Additionally, Linux does not need
to copy the initramfs into RAM (again) since the location where it is
mapped is usable as is and not marked as reserved.

Also, initrd files can now be placed in high subject memory (>4 G).

### Signed Block Stream (sbs) tools
The latest version of the sbs tools [4] enable the use of GnuPG keys
stored on Smartcards for signature generation. This version also adds
support for payload data extraction via the `sbs_inspect` tool.

## Mugenhwcfg and mugenhwcfg-live
The hardware XML config generation tool [5] has been extended to collect
CPUID information as well as (selected) MSRs. This additional collected
data provides more detailed information regarding the hardware platform
and is used to e.g. determine applicable MCUs or by SM (Subject Monitor)
for CPUID emulation.

Mugenhwcfg live [6] has been upgraded to Debian 12 (Bookworm) and
bundles the latest v0.7.2 of the `mugenhwcfg` tool.

If you are upgrading to the latest Muen v1.1.0 release, regeneration of
the hardware XML specification is required.

## Contrib
All external dependencies grouped under `contrib` have been updated to
their latest release version. Most notably, GRUB was updated to 2.12.

## Components
### Enable exception handling in Ada/SPARK subjects
The interrupt and exception handling routines of native Ada/SPARK
subjects have been extended such that they can also handle exceptions
themselves, e.g. page or protection faults. A Backtraces package is also
provided, which contains a basic implementation for analyzing the stack
and creating a call trace based on the information.

Furthermore, the component interrupt stack has been split from the
regular stack and must now explicitly be declared in the component XML
spec `<provides>` section.

### Subject Monitor
The SM component now leverages the additional hardware information
(CPUID, MSRs) in the XML policy to enhance emulation when monitored
subjects such as Linux inquire hardware capabilities. This allows to
indicate to Linux that certain FPU features are available.

Furthermore, the potential for time drift in RTC emulation has been
greatly diminished by expressing the CPU frequency in kHz instead of MHz
as well as making time calculations more robust.

### Libmutime
The time library now uses 128-bit arithmetic for timestamps to increase
precision. Furthermore, the algorithm described in [4] for converting
timestamps to dates and vice versa is used. It is the same algorithm
used by the Linux kernel. Besides being faster (as claimed in [4]),
SPARK is able to discharge all VCs.

### Linux
The support for Linux subjects has been updated for the current longterm
stable v6.1.82 kernel.

Also noteworthy is the vDSO support of the Muen clocksource. This
significantly speeds up Linux userspace calls for
`gettimeofday()`/`clock_gettime()`.

#### Muenfs
The muenfs Linux virtual filesystem driver has gained inode attribute
support. It is now possible to use the `chmod` and `chown` commands to
set access rights.

Furthermore, an example application is now provided that illustrates how
an event-driven, shared memory channel based service can be implemented
and in particular how to use the poll syscall in combination with
muenfs/channel events.

#### Muennet
The muennet Linux virtual network driver has gained support for child
devices and IRQ-driven reception and transmission.

### Solo5/MirageOS
The support for MirageOS unikernels has been update to Solo5 v0.8.0/ABI
version 3. This brings support for unikernel restart/reset using the
same SPARK initialization code as for native Ada/SPARK components.


## References
[1] - https://muen.sk/#documentation
[2] - https://gitlab.com/iucode-tool/iucode-tool
[3] - https://alire.ada.dev/
[4] - https://www.codelabs.ch/sbs-tools/
[5] - https://git.codelabs.ch/?p=muen/mugenhwcfg.git
[6] - https://github.com/codelabs-ch/mugenhwcfg-live/releases
[7] - https://github.com/cassioneri/eaf