From: Adrian-Ken Rueegsegger <ken@codelabs.ch>
Subject: [ANN] Muen development version 0.6 released
Date: Tue, 13 Jan 2015 10:17:54 +0100
Date: 2015-01-13T10:17:54+01:00 [thread overview]
Message-ID: <m92nr6$nbt$1@dont-email.me> (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
reply other threads:[~2015-01-13 9:17 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox