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 581398
To read all comments associated with this story, please click here.
RE: Comment by twitterfire
by thesunnyk on Wed 22nd Jan 2014 23:49 UTC in reply to "Comment by twitterfire"
Member since:

You're talking about a claim from the 90s. Microkernels certainly did have performance issues with single core 32-bit x86 architectures. This is where most of the testing was done to "prove" this claim. Modern architectures have a register file, which makes context switches cheaper, and many, many more cores, which makes multithreading kind of important. Monolithic kernel designs find it hard to distribute kernel-based drivers across cores.

I'm not saying Microkernels are definitely (comparatively) faster now, but that the conditions are very different, and the tests need to be redone under modern architectures.

Reply Parent Score: 4