[ANN] Muen development version 0.6 released

[Adrian-Ken Rueegsegger]

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

We are proud to announce the availability of Muen version 0.6, which
marks the first official development release.

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

* Migration of Muen to SPARK 2014

The kernel code has been migrated from SPARK 2005 to SPARK 2014 [1].
Absence of runtime errors is now verified using the GNATprove tool.
Switching to SPARK 2014 enables the use of a larger Ada language
subset and contracts are expressed as Ada 2012 aspects.
Replacing the SPARK 2005 annotations with Ada 2012 contracts made
the code much cleaner.

* PCI device passthrough using Intel VT-d (DMAR and IR)

Hardware passthrough is realized using Intel's VT-d DMA and
interrupt remapping technology. This enables the secure assignment
of PCI devices to subjects.

* XML policy abstraction and enhanced tool support

The XML system description has been modularized and additional
abstractions have been added to the policy. This enables users to
integrate complex component-based systems running on top of the Muen
kernel.

Further changes and improvements include:

* Support for Intel Haswell architecture
* Lightweight subject timer mechanism
* Scheduler improvements (minor frame synchronization)
* Subject Monitor migrated to SPARK 2014
* Debug server subject

Despite the addition of all these new features the kernel has retained
its small size. Some numbers regarding the size of Muen: the kernel
including the minimal zero-footprint runtime consists of a total of
5308 source lines of code (SPARK/Ada: 4979, Assembly: 329, as reported
by SLOCCount version 2.26).

A high-level document describing the process of configuring and building
a component-based system running on the Muen Separation Kernel is
available on the project website [2].

We would also like to mention that we gave a talk about Muen at the
High Integrity Software conference HIS 2014 [3] in Bristol. The slides
are available online at [4].

Further information is available on the project website [5] and the git
repository is at [6].

Please feel free to give the development version of Muen a try. Feedback
is much appreciated!

Kind regards,
Adrian

[1] - http://spark-2014.org/
[2] - http://muen.codelabs.ch/muen-toolchain.pdf
[3] - http://www.his-2014.co.uk/
[4] - http://www.slideshare.net/AdaCore/slides-his-2014secunethsr
[5] - http://muen.codelabs.ch/
[6] - http://git.codelabs.ch/?p=muen.git
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.12 (GNU/Linux)

iQIcBAEBCAAGBQJUtCG9AAoJEP/osUKX3goF7zoP/1dQYt75DvFnWSxgQzXTJQsE
6Pkc3kd/R/evA4CH+FtEHQ2qLNPrBG+H0QzD8gs9K5RY/rKy/YuIA+wWxDuiLPKL
2sLGzgk1An3exPxDvhypGFWdWW+sk10l+4EaqSljxDbVBJvBD+LkryH9tZhxZHho
X7EoO46DzNzRNLROlGBUoNb0K4rr8XbWDLi0vgvYL5Desvs1fCmShfCXqd6LEz0t
F7rcD/gzBEaQe5UI15xMe26xNBqUURc3Q1ogv4VgijnaLXQtckytaW6WyVxdj4By
DqQDfJ0R2FAyk5N4c6XXONGbtofhibQIcJmi5td8KPYbsFD07bS2KLTXE/vabIJW
kcnEORoI62i1JFDYMqdxQncGkcUf3Ai98xjBTtZBl/b/HN68gP3siFoyhqUavCTQ
rriVYy1hIQfH3NmrApmEyxJn9KYjmAdrKBKUG0+pZsz5siV8KbzoSR77osfjE50w
qvSDTArAjsUM4Es6qj/5aD75p4OKbbM+nJ1rt2aajVMYoRNEqGMVLloBByFhY2WT
1WkOz4xETcxVSdZL28jPp6ewOXc6cE/pCQJGZ59SVQFrqoCrufV9O19oOH2l98dJ
EHWh8BmCXCoG2H/NkgJdi6y5EqPbseCvJPKC5MLXRqAIyJYnfxXahgV8q33PszTU
rrSVv6gR9Wtj6sNXRY7s
=bikG
-----END PGP SIGNATURE-----