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 581401
To read all comments associated with this story, please click here.
The SWISS
by hackus on Thu 23rd Jan 2014 00:31 UTC
hackus
Member since:
2006-06-28

have been drinking spiked hot coco while they wrote their formalisms of correctness.

http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleten...

-Hackus

Reply Score: 1

RE: The SWISS
by kwan_e on Thu 23rd Jan 2014 01:04 in reply to "The SWISS"
kwan_e Member since:
2007-02-18

have been drinking spiked hot coco while they wrote their formalisms of correctness.

http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleten...

-Hackus


That only applies if they claimed to be both complete and correct. They can very well claim to be correct as long as they don't claim completeness.

What you may be looking for is the halting problem.

Reply Parent Score: 3

RE[2]: The SWISS
by pgeorgi on Thu 23rd Jan 2014 06:42 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: The SWISS
by galvanash on Thu 23rd Jan 2014 04:52 in reply to "The SWISS"
galvanash Member since:
2006-01-25

have been drinking spiked hot coco while they wrote their formalisms of correctness.

http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleten...

-Hackus


They do not claim "correctness" in the mathematical sense. They simply guarantee exactly what is in the quote in the parent article:

has been formally proven to contain no runtime errors at the source code level.


That is not at all the same thing as proving correctness... Read the article before judging, because if you look into the track record of the SPARK language and you consider the kernels design (extremely high reliance on hardware supplied isolation features, extremely small code footprint, a plethora of self imposed restrictions by the language, etc.), proving the simple statement above does not sound all that far fetched to me.

Keep in mind this is kernel is written in a language that self-imposes the following restrictions:

No access types (pointers)
No recursion
No exceptions
No goto
No anonymous and aliased types
No functions with side-eff ects
No dynamic array bounds
No dynamic memory allocation
No dynamic dispatch

Its basically a static system - address spaces usage and all allocations are done through static configuration, not code. It isn't all that hard to validate because the language is so restrictive that virtually any form of dynamic behavior by code at runtime is impossible.

Useful for some things? Maybe so. Competition for other more conventional kernel designs? Um, no. Its really apples and oranges - this is for building absolutely bullet proof embedded systems, its too weird for anything else...

Edited 2014-01-23 04:54 UTC

Reply Parent Score: 5

RE[2]: The SWISS
by moondevil on Thu 23rd Jan 2014 09:06 in reply to "RE: The SWISS"
moondevil Member since:
2005-07-08

You have the same restrictions when writing compliant MISRA C code, which is required for environments where human life's are at risk.

Reply Parent Score: 4