* [ANN] Muen development version 0.6 released
@ 2015-01-13 9:17 Adrian-Ken Rueegsegger
0 siblings, 0 replies; only message in thread
From: Adrian-Ken Rueegsegger @ 2015-01-13 9:17 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2015-01-13 9:17 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2015-01-13 9:17 [ANN] Muen development version 0.6 released Adrian-Ken Rueegsegger
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox