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.

Thread beginning with comment 581421
To view parent comment, click here.
To read all comments associated with this story, please click here.
RE[2]: The SWISS
by pgeorgi on Thu 23rd Jan 2014 06:42 UTC in reply to "RE: The SWISS"
pgeorgi
Member since:
2010-02-18

What you may be looking for is the halting problem.

SPARK 2014 (which Muen doesn't use yet) attempts to attack the halting problem with loop variants. By proving that all loops terminate at some point, you can show that all blocks of code terminates eventually.
In case of an operating system kernel, you will still have an endless outer loop, since you don't want the entire system to terminate after a well-defined number of steps.

And it's not even the first language that eliminates the halting problem. For example, DTrace's script language is also safe since it only allows loops with predefined iteration boundaries and forward jumps.

Neither language is turing complete (in case of SPARK 2014: if you choose to use loop variants), but many solutions to problems don't need this kind of power, so you can still write meaningful code within this constraint.

Reply Parent Score: 3

RE[3]: The SWISS
by kwan_e on Thu 23rd Jan 2014 07:44 in reply to "RE[2]: The SWISS"
kwan_e Member since:
2007-02-18

The halting problem doesn't prevent specific classes of failures being proven/disproven.

Reply Parent Score: 3

RE[4]: The SWISS
by pgeorgi on Thu 23rd Jan 2014 11:08 in reply to "RE[3]: The SWISS"
pgeorgi Member since:
2010-02-18

I was only meaning to point out that even the halting problem isn't as universal as pop computer science likes to make it.

Reply Parent Score: 3

RE[4]: The SWISS
by Alfman on Thu 23rd Jan 2014 17:56 in reply to "RE[3]: The SWISS"
Alfman Member since:
2011-01-28

kwan_e,

"The halting problem doesn't prevent specific classes of failures being proven/disproven."

Many people learned about the halting problem in absolute terms and don't seem to get this. I'd say the over-generalization of the halting problem's conclusions over all algorithms classes makes it one of the most abused concepts of CS.

The set of all algorithms:
1. contain self contradictions.
2. contain no self contradictions.

The halting problem only proves there's no solution for those in #1. By extension, it proves there's no solution for the most general combined set of #1 and #2. However it says nothing about the feasibility of halting solutions for #2.



Q: Just for fun, does this function halt or not halt?

function F(int x) {
return x==0? x : F(x-1);
}


A1: Mathematician - It only halts for non-negative inputs. Negative inputs will loop infinitely as x approaches minus infinity.

A2: Computer scientist - It always halts due to the eventual stack overflow on a real machine.

A3: Computer scientist - It always halts due to the eventual integer wrap around on a real machine.

A4: Physicist - It always halts because running it infinitely would require more energy than exists in the universe.

Reply Parent Score: 3