[ANN] Muen development version 0.8 released

[Adrian-Ken Rueegsegger <ken@codelabs.ch>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

We are proud to announce the availability of Muen version 0.8.

The following major features and improvements have been implemented
since the last release:

=== Subject Lifecycle

With the implementation of a subject loader (SL) component it is now
possible to reset and restart subjects at runtime with minimal support
from the kernel.

The new loader policy abstraction eases the specification of loader
subjects which control the lifecycle of one or multiple subjects.
Aside from the state, loaders have access to the entire address space
of a managed subject in order to be able to set up the execution
environment.

The new SL component written in SPARK 2014 initializes/resets the
writable memory regions of its associated subjects. To find the actual
memory regions to process, the loader consults each monitored subject
info region by querying it using the new subject info (sinfo) client
library. Prior to starting execution of a monitored subject, integrity
hashes of each memory region are calculated and compared to their
reference value provided by the sinfo data.

The demo system has been adapted to make use of this new
functionality: the NIC Linux can be restarted by pressing the Right
Control+F10 key combination.

=== System reboot/shutdown

The introduction of a new 'kernel' event mode and event actions for
system reboot and poweroff enables policy writers to grant subjects
the capability to initiate a system reboot or shutdown. If a subject
triggers a reboot event, the kernel performs a power-cycle using the
Reset Control Register (I/O port 0xcf9). The shutdown functionality is
implemented by performing an ACPI shutdown using the poweroff port and
the PM1A Control Sleep Type capability.

As with the subject restart, the demo system has been extended to
showcase the new feature: a system reboot can be triggered by pressing
the Right Control+F11 keys while Right Control+F12 initiates a shutdown.

=== Policy & Toolchain improvements

The Muen policy has been extended with a config section which enables
the parametrization of a system via the declaration of configuration
values.
Boolean expressions referencing existing config values can be used to
formulate additional properties. The introduction of conditionals that
reference config values or expressions selectively enable/disable
parts of the policy which allows for flexible customization of a
system at integration time.

To increase the expressiveness of the policy and ease native component
development, component descriptions have been extended with the
library construct including dependency declaration. Additionally it is
now possible to declare logical devices as well as memory and channel
array resources. The new component spec generation tool reads the
description of a given component and generates Ada/SPARK packages
containing constants of the declared logical component resources.
These generated specifications can be used in the component source
code to access the declared resources. This ensures a consistent view
of the system according to the policy.

Physical memory regions can now optionally declare an integrity hash.
The SHA-256 hash value can be used to verify the initial content of a
given region at runtime. A tool has been implemented that calculates
hashes for all physical regions with content (file or pattern). The
region hashes are exported as part of the subject info data and used
by the SL as described above.

=== Kernel improvements

To prevent potential issues related to Intel Hyper-Threading, e.g.
side-channels, the kernel now only activates one thread per physical
CPU core. CPUID leaf 11 (Extended Topology Enumeration Leaf) is used
to determine the SMT ID of each logical CPU and deactivate it if the
ID is non-zero. This effectively disables HT even if no such option is
present in the BIOS.

Feature-wise, support for event actions has been added. The improved
functionality increases the flexibility of the event mechanism and
facilitates subject lifecycle management as well as system restart and
shutdown.

Many other improvements and stabilizations such as e.g. replacement of
assembler code with SPARK and reduction of stack size to 4K have been
implemented.

=== Further changes and improvements include

 * Support for 32-bit Windows VMs using Genode/Virtualbox
 * Support for Intel Broadwell and Skylake microarchitecture
 * Support for PCI multi-function device pass-through
 * Implement tool to statically calculate worst-case stack usage
 * Implement tool to generate scheduling plans
 * Implement subject info client library in SPARK 2014
 * Update of Linux kernel to version 4.6
 * Add support for multiple initramfs per Linux subject

With the advent of subject lifecycle management, system shutdown and
reboot support and the numerous toolchain improvements, the Muen
platform is getting more and more mature. The continuous enhancement
and refinement of system policy abstractions, especially the
components construct, further simplifies the system specification
process and enables the description of complex systems composed of a
large number of subjects.

We are also thrilled that this release includes the previously
announced [1] support for execution of hardware-accelerated 32-bit
Windows VMs on top of the Muen SK through the use of Genode/VirtualBox
as a deprivileged VMM. A detailed description of the architecture and
an account of how this feature came to be can be found in the Genode
16.08 release notes [2].

Last but not least we would like to thank Christiane Kuhn for her
contribution of the scheduling plan generation tool [3] which she
developed as part of a student project/internship.

Further information about Muen is available on the project website [4]
and the git repository can be found at [5].

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

Kind regards,
The Muen Team

[1] - https://groups.google.com/forum/#!topic/muen-dev/ln7ZrIfDk8c
[2] -
https://genode.org/documentation/release-notes/16.08#VirtualBox_4_on_top
_of_the_Muen_separation_kernel
[3] - https://git.codelabs.ch/?p=muen/mugenschedcfg.git
[4] - https://muen.codelabs.ch/
[5] - https://git.codelabs.ch/?p=muen.git

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2

iQIcBAEBCAAGBQJYmMCtAAoJEMEf4lxkugAyZosP/R0pPd5XgIWKLlN7pIomR4yv
mbGk4cP1bBE7KdirdP5Q6FajFCnA+yyP48pfYesiDewXMfLwZqf7CjPIEhtnmfaH
kjZYljoUnsZQjak5uvRi426XYWfBTcrnTv7oyfJd2MPkiH7OjYikfG3YVd9L7VFc
s1nsqsNh+nw4aifMxp1fhEgIporgACN6rnIlMl/zMLKcYRYguCmqnShhC73ukuj6
yXjLO+gSShVFUr3zzD0/LdUUNNw/PQfXFIotY/lVqt3GP45+VZ49ZFsCGm+es0re
DADFSgz3u2M9LHzG089RY4WObKyxrNQdxgb2+v66edmOyGSAtEWZrmI89SgLQFtM
w4ETjU4wFtd5mG5JZNYBCWs3JqgrD0g89jH3t+XgpeWzJnF2rTtsSITCApx6DiOg
QQKVL/yK5rhEezax6W3wwJ0XCBjfwz8ubZQjURHprrVbWPSbhSpl0pu879iI1Ynn
FFvYul9YcxG4FvWjY5y3lpyHVYwRV2NO+MUtQYyURg9Q6lw0EOfHeE/7sQTnQA3Q
xBtjQnBzOObbDURecTvKsr/AcHQ5lMEjfv8Isvbu1sT43sfp8c60LYiMeXDuiwDk
VXbDK54ZRmCz8zbZUbeOEKW6V2tiCmGWw7rgtNimDCSlqiKwak5z1T8kekP7XtX4
VRxUdN1lO/OGNzzo0fqN
=jKON
-----END PGP SIGNATURE-----