From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 border1.nntp.dca3.giganews.com!backlog3.nntp.dca3.giganews.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!goblin1!goblin.stu.neva.ru!eternal-september.org!feeder.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Adrian-Ken Rueegsegger <ken@codelabs.ch>
Newsgroups: comp.lang.ada
Subject: [ANN] Muen - An x86/64 Separation Kernel for High Assurance
Date: Tue, 10 Dec 2013 18:25:20 +0100
Organization: A noiseless patient Spider
Message-ID: <l87ipv$u54$1@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit
Injection-Date: Tue, 10 Dec 2013 17:25:19 +0000 (UTC)
Injection-Info: mx05.eternal-september.org;
 posting-host="9f812117a11302d37d167ac7bcaea95c";
 logging-data="30884"; mail-complaints-to="abuse@eternal-september.org";
 posting-account="U2FsdGVkX188tk/AGP3VHpeBGM0JeI5w"
User-Agent: Mozilla/5.0 (X11; Linux x86_64;
 rv:17.0) Gecko/20131103 Icedove/17.0.10
Cancel-Lock: sha1:gvmQINzB9rrMTX6ocVXkOe9qfVQ=
X-Original-Bytes: 2756
Xref: number.nntp.dca.giganews.com comp.lang.ada:184165
Date: 2013-12-10T18:25:20+01:00
List-Id: <comp.lang.ada>

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