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_INFOIA32_THERM_STATUSIA32_TEMPERATURE_TARGETIA32_PACKAGE_THERM_STATUSMSR_RAPL_POWER_UNITMSR_PKG_POWER_LIMITMSR_PKG_ENERGY_STATUSMSR_DRAM_ENERGY_STATUSMSR_PP1_ENERGY_STATUSMSR_CONFIG_TDP_CONTROLIA32_PM_ENABLEIA32_HWP_CAPABILITIESIA32_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:
virtualAddressfor memory regions and channelseventandvectornumbers 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] - Muen | SK for x86/64
[2] - iucode-tool / iucode-tool · GitLab
[3] - https://alire.ada.dev/
[4] - Signed Block Stream (SBS) Tools
[5] - git.codelabs.ch Git - muen/mugenhwcfg.git/summary
[6] - Releases · codelabs-ch/mugenhwcfg-live · GitHub
[7] - GitHub - cassioneri/eaf: Supplementary material to "Euclidean Affine Functions and their Application to Calendar Algorithms"