[ANN] Muen - An x86/64 Separation Kernel for High Assurance

[Adrian-Ken Rueegsegger <ken@codelabs.ch>]

Hi,

We are proud to announce the public availability of the Muen Separation
Kernel project. The goal of the Muen project is the development of a
trustworthy open-source foundation for component-based high-assurance
systems.

The name Muen is a Japanese term that translates to "unrelated" or
"without relation" which makes for a nice allegory of the main objective
of a Separation Kernel. A Separation Kernel (SK) is a specialized
microkernel that provides an execution environment for components that
exclusively communicate according to a given security policy and are
otherwise strictly isolated from each other.

The Muen kernel has been implemented in SPARK and runs on the Intel
x86/64 architecture employing hardware-assisted virtualization (VT-x) as
the fundamental separation mechanism.

The following major features have been realized in the first milestone:

* Minimal SK for the Intel x86/64 architecture written in the SPARK language
* Full availability of source code and documentation
* Proof of absence of runtime errors
* Multicore (SMP) support
* Nested paging (EPT) and memory typing (PAT)
* Fixed cyclic scheduling using Intel VMX preemption timer
* Static assignment of resources according to system policy
* Event mechanism
* Minimal Zero-Footprint Run-Time (RTS)
* Support for 64-bit native and 32-bit VM components
* A demo system involving an xv6 VM and a native crypto component

The project website can be found at [1] and the git repository is
available under [2]. A snapshot of the Muen repository can be downloaded
from [3].

Kind regards,
Adrian

[1] - http://muen.codelabs.ch/
[2] - http://git.codelabs.ch/?p=muen.git
[3] - http://git.codelabs.ch/?p=muen.git;a=snapshot;h=master;sf=zip