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 581420
To read all comments associated with this story, please click here.
RE: I wonder about that claim
by pgeorgi on Thu 23rd Jan 2014 06:35 UTC in reply to "I wonder about that claim"
pgeorgi
Member since:
2010-02-18

My uni lecturer has been involved in SEL4 http://ssrg.nicta.com.au/projects/seL4/ which also claims to be the first design to use formal methods to verify security. Maybe they just don't know about each other but it appears one of them has to be wrong.

The important qualifier in the Muen statement is "Open Source" - there are a number of formally verified kernels out there, but none are Open Source.

Reply Parent Score: 4