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.
To read all comments associated with this story, please click here.
Member since:
2010-02-18
It's not just a microkernel, it's a separation kernel.
The techniques are similar (and so claiming it's a microkernel, as happens on the website isn't wrong), but the system you end up with is quite different from your ordinary microkernel design.
The project is _all_ about security.
For example, it's built around a fixed process scheduler to reduce side channels that are based on CPU use. From a performance point of view, you just Don't Do That[tm].
Edited 2014-01-23 06:31 UTC