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

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

[Adrian-Ken Rueegsegger]

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

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

[Jacob Sparre Andersen]

Adrian-Ken Rueegsegger wrote:

> 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.

This sounds very good!

I look forward to try Muen.

Greetings,

Jacob
-- 
»Great minds discuss ideas,
 Average minds discuss events,
 Small minds discuss people.«

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

[Maciej Sobczak]

W dniu wtorek, 10 grudnia 2013 18:25:20 UTC+1 użytkownik Adrian-Ken Rueegsegger napisał:

> 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.

Interesting.

Do you plan to support the TCP/IP stack in this kernel?
(It is announced as a prototype, so I assume that it is not yet done.)

-- 
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com

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

[Adrian-Ken Rueegsegger]

On 12/11/2013 03:07 PM, Maciej Sobczak wrote:
> W dniu wtorek, 10 grudnia 2013 18:25:20 UTC+1 użytkownik Adrian-Ken Rueegsegger napisał:
> 
>> 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.
> 
> Interesting.
> 
> Do you plan to support the TCP/IP stack in this kernel?
> (It is announced as a prototype, so I assume that it is not yet done.)

No, the kernel will not have a TCP/IP stack. Networking must be done by
a subject running on top of the Muen Kernel, e.g. a Linux VM that has
direct access to a network card. A second possibility would be to
implement TCP/IP as a native Ada/SPARK component which would drive the
NIC directly. AdaCore has such a stack, see [1].

Regards,
Adrian

[1] - http://www.adacore.com/labs/tcp-ip-stack/

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

[Eryndlia Mavourneen]

On Wednesday, December 11, 2013 8:46:02 AM UTC-6, Adrian-Ken Rueegsegger wrote:
> On 12/11/2013 03:07 PM, Maciej Sobczak wrote:
> > W dniu wtorek, 10 grudnia 2013 18:25:20 UTC+1 użytkownik Adrian-Ken Rueegsegger napisał:
> > 
> >> 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.
> > 
> > Interesting.
> > 
> > Do you plan to support the TCP/IP stack in this kernel?
> > (It is announced as a prototype, so I assume that it is not yet done.)
> 
> No, the kernel will not have a TCP/IP stack. Networking must be done by
> a subject running on top of the Muen Kernel, e.g. a Linux VM that has
> direct access to a network card. A second possibility would be to
> implement TCP/IP as a native Ada/SPARK component which would drive the
> NIC directly. AdaCore has such a stack, see [1].
> 
> Regards,
> Adrian
> 
> [1] - http://www.adacore.com/labs/tcp-ip-stack/

Hear hear!  I definitely agree that the kernel should be kept clean, efficient, and safe.  Protocols and the such should be implemented within layers outside of the kernel.

-- Eryndlia Mavourneen (KK1T)

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

[Marc C]

On Tuesday, December 10, 2013 11:25:20 AM UTC-6, Adrian-Ken Rueegsegger wrote:
> 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.

This was posted in /r/programming on Reddit and generated some decent discussion. http://redd.it/1sjyop

Marc A. Criley
Ada sub-reddit moderator

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

[Diogenes]

Will this kernel function on any AMD based systems or any embedded systems (Gumstix, Rasberry Pi)?

Are there plans to port this kernel?

Are you looking for contributors?

Diogenes

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

[Alexander Senier]

On Fri, 13 Dec 2013 13:41:38 -0800 (PST)
Diogenes <phathax0r@gmail.com> wrote:

> Will this kernel function on any AMD based systems or any embedded
> systems (Gumstix, Rasberry Pi)?

Muen purposely is a relatively small layer on top Intel VT as this
keeps the kernel complexity low. Supporting AMD-based systems should be
possible, though, with reasonable effort and a minor increase in
complexity as AMD's hardware virtualization features are comparable.

When it comes to embedded targets the closest match seems to be the
Intel Atom CPU. While versions with VT-x exist, there are currently no
Atom CPUs with EPT or VT-d. EPT (aka. nested paging) is an important
feature to reduce the complexity (and performance) of virtual machines.
VT-d is essential if untrusted virtual machines have direct access to
PCIe devices and especially if you want to build a system that uses
untrusted device drivers / devices in conjunction with trusted
applications (think of an untrusted Linux VM that drives the network
card and a trusted application that enforces encryption of all
traffic). Should Intel ever build VT-d (and EPT) into Atom CPUs, a Muen
port to these CPUs is thinkable.

> Are there plans to port this kernel?

While a port to a suitable AMD CPU seems doable, it is not planned at
the moment as there is no demand. Given the size of the kernel, a port
to completely different architectures like ARM would probably be more
complex than a rewrite.

> Are you looking for contributors?

Sure. Note, that Muen is meant to be the foundation for trustworthy
*systems* - in a component-based system there are many other interesting
areas outside the kernel. Someone asked for a (trusted?) TCP/IP stack
earlier, other trusted components (input, graphics, crypto…) are
necessary to make up a complete system.

Regards
Alex

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

[Diogenes]

On Friday, December 13, 2013 6:30:54 PM UTC-5, Alexander Senier wrote:
> On Fri, 13 Dec 2013 13:41:38 -0800 (PST)
> 
> Diogenes <phathax0r@gmail.com> wrote:
> 
> 
> 
> 
> > Are there plans to port this kernel?
 
> While a port to a suitable AMD CPU seems doable, it is not planned at
> 
> the moment as there is no demand. Given the size of the kernel, a port
> 
> to completely different architectures like ARM would probably be more
> 
> complex than a rewrite.
> 
> 
> 
> > Are you looking for contributors?
> 
> 
> 
> Sure. Note, that Muen is meant to be the foundation for trustworthy
> 
> *systems* - in a component-based system there are many other interesting
> 
> areas outside the kernel. Someone asked for a (trusted?) TCP/IP stack
> 
> earlier, other trusted components (input, graphics, crypto…) are
> 
> necessary to make up a complete system.
> 
> 
> 
> Regards
> 
> Alex

Thanks. I was curious because I'm working on some Ada apps for both Opteron and Android platforms.

I'll download your kernel and have look.

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

[Adrian-Ken Rueegsegger]

On 12/14/2013 12:30 AM, Alexander Senier wrote:
> On Fri, 13 Dec 2013 13:41:38 -0800 (PST)
> Diogenes <phathax0r@gmail.com> wrote:
[...]
>> Are you looking for contributors?
> 
> Sure. Note, that Muen is meant to be the foundation for trustworthy
> *systems* - in a component-based system there are many other interesting
> areas outside the kernel. Someone asked for a (trusted?) TCP/IP stack
> earlier, other trusted components (input, graphics, crypto…) are
> necessary to make up a complete system.

A minor addition to what Alex already said: if you want to contribute,
feel free to join the project mailing list [1] for discussions and
patche submission.

Regards,
Adrian

[1] - http://muen.codelabs.ch/#_resources

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

[Brian Drummond]

On Fri, 13 Dec 2013 15:39:41 -0800, Diogenes wrote:

> On Friday, December 13, 2013 6:30:54 PM UTC-5, Alexander Senier wrote:
>> On Fri, 13 Dec 2013 13:41:38 -0800 (PST)
>> 
>> Diogenes <phathax0r@gmail.com> wrote:
>> 
>> 
>> 
>> 
>> > Are there plans to port this kernel?
>  
>>  Given the size of the kernel, a port
>> 
>> to completely different architectures like ARM would probably be more
>> 
>> complex than a rewrite.

> Thanks. I was curious because I'm working on some Ada apps for both
> Opteron and Android platforms.

What does your toolchain for Android look like?

Last time I looked (around Android 2.3) the Dragonlace compiler built 
successfully to generate (command line) apps on Android but there were no 
signs of imminent success getting Ada through the NDK to talk to the GUI.

Which compiler (NDK version etc) are you using, and which Android 
versions?

Thanks,
- Brian

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

[Brian Drummond]

On Fri, 13 Dec 2013 15:39:41 -0800, Diogenes wrote:

> On Friday, December 13, 2013 6:30:54 PM UTC-5, Alexander Senier wrote:
>> On Fri, 13 Dec 2013 13:41:38 -0800 (PST)
>> 
>> Diogenes <phathax0r@gmail.com> wrote:
>> 
>> 
>> 
>> 
>> > Are there plans to port this kernel?
>  
>>  Given the size of the kernel, a port
>> 
>> to completely different architectures like ARM would probably be more
>> 
>> complex than a rewrite.

> Thanks. I was curious because I'm working on some Ada apps for both
> Opteron and Android platforms.

What does your toolchain for Android look like?

Last time I looked (around Android 2.3) the Dragonlace compiler built 
successfully to generate (command line) apps on Android but there were no 
signs of imminent success getting Ada through the NDK to talk to the GUI.

Which compiler (NDK version etc) are you using, and which Android 
versions?

Thanks,
- Brian