Linked by Thom Holwerda on Wed 22nd Jan 2014 13:47 UTC, submitted by fran
OSNews, Generic OSes

The Muen Separation Kernel is the world's first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. It is developed in Switzerland by the Institute for Internet Technologies and Applications (ITA) at the University of Applied Sciences Rapperswil (HSR). Muen was designed specifically to meet the challenging requirements of high-assurance systems on the Intel x86/64 platform. To ensure Muen is suitable for highly critical systems and advanced national security platforms, HSR closely cooperates with the high-security specialist secunet Security Networks AG in Germany.

The webpage contains instructions for building the kernel yourself, for installing it in a virtual machine, and for running it on real hardware.

Permalink for comment 581462
To read all comments associated with this story, please click here.
RE: What about performance?
by pgeorgi on Thu 23rd Jan 2014 13:48 UTC in reply to "What about performance?"
pgeorgi
Member since:
2010-02-18

I´m not talking about the microkernel design but the programming language. Linux uses dirty tricks in C and in some cases assembler to optimize as much as possible. Can you match that performance in a restricted language like Spark?

The first time I looked at the Muen code, I wondered "where is this thing actually doing something?"

The answer is that it pushes lots of things to compile time and hardware. The scheduler runs a fixed schedule. Memory mappings are compiled in. The Ada runtime checks can be disabled since SPARK makes sure the code never runs into them. Isolation is provided by VT-x.

All that makes Muen a really special kernel for really special purposes, which is why that sort of kernel has a special name: Separation Kernel.
But there's a place for it. The academic work in that field goes back to the late 60s, and there's still nothing better for situations where you _really_ _really_ want to make sure that data doesn't bleed from one process ("subject") to another - except running each process on its own processor with its own RAM, which is what Separation Kernels seek to emulate.

Reply Parent Score: 3