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 581434
To read all comments associated with this story, please click here.
RE[7]: Comment by twitterfire
by hackus on Thu 23rd Jan 2014 10:48 UTC in reply to "RE[6]: Comment by twitterfire"
hackus
Member since:
2006-06-28

I think given the breath of devices LINUX currently runs on that it is self evident, that of course, it IS one solution for just about any problem you can think of.

Despite your comment about growing up, you are not going to change reality.

It is a fact that LINUX exists in all realms and works equally well.

No way are you going to get a correct, nor a complete solution to a formalized kernel of any kind.

I don't care what it is, Micro or Monolithic.

That being said Monolithic is currently and will forever reign supreme on von Neumann machines, not from just a scalibility approach which is SELF EVIDENT, but also from a cost one as well.

I would also like to point out complete also infers secure.

Not going to happen, even LINUX isn't secure and never will be in those terms. (Formalized.)

-Hack

Reply Parent Score: 1