[ANN] Muen development version 0.8 released

[ANN] Muen development version 0.8 released

[Adrian-Ken Rueegsegger]

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

Re: [ANN] Muen development version 0.8 released

[Vincent]

Le lundi 6 février 2017 19:29:53 UTC+1, Adrian-Ken Rueegsegger a écrit :
> 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:
> 

Thank you very much for this very impressive work. I have a few questions regarding the use of Muen :  

1. I understand that this separation Kernel is an hypervisor, but how does
   it compare to other hypervisor like for instance the one from Wind River ?
   Does Muen allows hard Real Time softwares ? What kind of scheduling does
   the Muen kernel ?

2. How does Muen compare to solutions like Linux KVM ? How does it compare
   to Xen ?

3. Will it be possible to use Muen with the future OpenVMS on x86-64 ?

Kind regards,

Vincent DIEMUNSCH
 

Re: [ANN] Muen development version 0.8 released

[Adrian-Ken Rueegsegger]

Hello Vincent,

On 02/09/2017 01:40 PM, Vincent wrote:
> Le lundi 6 février 2017 19:29:53 UTC+1, Adrian-Ken Rueegsegger a écrit :
>> 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:
>>
> 
> Thank you very much for this very impressive work. I have a few questions regarding the use of Muen :  

Glad that you like our project!

> 1. I understand that this separation Kernel is an hypervisor, but how does
>    it compare to other hypervisor like for instance the one from Wind River ?
>    Does Muen allows hard Real Time softwares ? What kind of scheduling does
>    the Muen kernel ?

I am not sure how to best answer this question since I do not know the
Wind River Hypervisor. Looking at the product information online some of
the features are quite similar while in other areas there are differences.
Since I am not in a position to make a meaningful comparison, let me
instead list some of the features of Muen to give you a better picture:

= Static resource allocation
One of the main design choices of the Muen Separation Kernel and systems
build on top of it is, that all system resources such as memory,
devices, CPU time etc are assigned to subjects via the system policy at
integration time. As a consequence, systems have a static structure
which does not change during runtime. This means that the SK does not
perform any dynamic resource allocation at runtime, which greatly
simplifies the kernel design and implementation.
Note that Muen has support for Intel VT-d (DMA and Interrupt remapping)
which facilitates PCI device pass-through.

= Multicore support
All cores provided by a hardware platform can be used for subject execution.

= Scheduling
Muen implements a fixed, cyclic scheduler. Execution order and time
assignment of each subject is specified in the system policy. The kernel
enforces the scheduling plan during runtime by executing each subject
for the alloted time and then (preemptively) switching to the next one.

= Subject execution environment
Since Muen employs Intel Virtualization Extensions (VT-x) incl.
Unrestricted Guest Support and Nested Paging/Extended Page Tables (EPT)
as a basic mechanism to execute and separate subjects, it can run many
different types of subjects:

- Native 64-bit Ada & SPARK 2014 subjects
- Linux 32/64-bit VMs
- Genode x86_64 base-hw system
- Windows 32-bit VMs (by means of Genode/VirtualBox)

A subject execution environment can be further customized in the system
policy, e.g. allow access to the Timestamp Counter (TSC).

= Small size and low complexity
During the development of Muen we took deliberate design choices to
minimize the overall kernel complexity. The simplification drastically
reduces code size which is illustrated by the current, tiny kernel size
of ~5'500 sloc. This make the kernel suitable for formal verification.
On the other hand, a consequence is that the supported feature set is
smaller than what you get from a general purpose/dynamic hypervisor.
Here are two examples of restrictions imposed by Muen:

- Subjects are not allowed to migrate between CPU cores
- Muen only runs on recent x86_64 hardware with Intel VT-x and EPT support

Aside from these features there are some additional points that we think
are important.

= Availability of code & documentation
Muen is an open source project and we publish all code and
documentation. We think it is paramount for an SK to be independently
inspectable since it is always part of the Trusted Computing Base (TCB)
of any system built on top of Muen.
The small size makes it realistically possible to read and understand
the entire Muen kernel code.

= Formal Verification
Since Muen is implemented in SPARK 2014, we prove full absence of
runtime errors at the source code level. Since we publish the entire
source code and because the SPARK GPL toolchain by AdaCore is freely
available, everybody can independently reproduce these proofs in their
own environment.

> 2. How does Muen compare to solutions like Linux KVM ? How does it compare
>    to Xen ?

Similar to the first question it is not so easy to compare Muen to a
fully fledged hypervisor such as KVM and Xen since it is comparing
apples with oranges. Xen and KVM are fully-fledged hypervisors which
feature dynamic VM construction and deconstruction, live migration etc.
With Muen systems you have to take more of an embedded system
development approach, where you know your target hardware platform and
system structure at integration time.

I think in the end it comes down to this: since Muen is a Separation
Kernel it (intentionally) does not address all use cases targeted by
general purpose hypervisor.

> 3. Will it be possible to use Muen with the future OpenVMS on x86-64 ?

I have no prior experience with OpenVMS. Since there are no inherent
restrictions imposed by Muen on the kind of subjects that can be
executed it should in principle be possible. However, without more
technical information and access to OpenVMS x86-64 there is no way for
me to estimate the required porting effort.

I hope I was able to answer your questions.

Best regards,
Adrian

PS: If you have more questions regarding Muen there is also a project
mailing list, see [1].

[1] - https://muen.sk/#mailing-list

Re: [ANN] Muen development version 0.8 released

[vincent.diemunsch]

Le lundi 13 février 2017 18:07:24 UTC+1, Adrian-Ken Rueegsegger a écrit :
> 
> I hope I was able to answer your questions.
> 
> Best regards,
> Adrian
> 
> PS: If you have more questions regarding Muen there is also a project
> mailing list, see [1].
> 
> [1] - https://muen.sk/#mailing-list

Thank you very much Adrian for this complete answer.
I will take time to study Muen a little bit more !
Kind regards,

Vincent