[ANN] Muen development version 0.6 released

[ANN] Muen development version 0.6 released

[Adrian-Ken Rueegsegger]

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