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 581455
To read all comments associated with this story, please click here.
RE[6]: The SWISS
by pgeorgi on Thu 23rd Jan 2014 13:10 UTC in reply to "RE[5]: The SWISS"
Member since:

Pop computer science? Is Alan Turing pop computer science?

No, but many interpretations of "X is impossible because of Y" where Y is some classic CS theorem are.

It is a matter of mathematical proof that there can be no method of checking whether an arbitrary program will halt.

You certainly can't build a turing machine emulator in those languages. So yes, arbitrary programs are out.

Not even SPARK 2014 can catch all non-terminating loops. It can either be too restrictive and only limit you to a very small subset, or catch too many false-positives.

It is "too restrictive". The idea is that it's still good enough for some meaningful operations - also, loop variants aren't enforced everywhere by the language (but only where you annotate them): as said, the outer loop of an operating system kernel's scheduler will run "endlessly" with a non-deterministic exit (shutdown event).
But being able to show that everything else does return, so at some point, the processor ends up in the main loop again, is already very useful.

Dtrace enforces that scripts terminate eventually with no exceptions, but it's a very special purpose language. It's still very useful to its users, so the "very small subset" is good enough.

It's designed to be used on production systems, messing with the kernel, so I'd rather have one level of safety more rather than expressiveness I barely need. It's a good trade-off.

(and all these constraints keep hardware bugs out of the question. Trying to model these will be so complex as to be useless...)

Reply Parent Score: 3