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 581402
To view parent comment, click here.
To read all comments associated with this story, please click here.
RE[5]: Comment by twitterfire
by hackus on Thu 23rd Jan 2014 00:49 UTC in reply to "RE[4]: Comment by twitterfire"
hackus
Member since:
2006-06-28

Because it is stupid?

This argument has been going on for DECADES, by stupid people who need money to keep their stupid cash donors convinced of the "benefits" and "possibilities" without anything going anywhere and no research to show for it.

In short, we need money to write more papers and buy chicken.

This is how I look at it:

You cannot define a system of logic that is not capable of self contradiction.

So first of all, you cannot have a formalism in Computer Science that will yield a perfect program.

It will NEVER happen.

This problem was solved and put to rest by men that are far more brilliant than those born today with corn syrup, anti depressants and rittalin stringing through their brains with the attention span of a teetse fly.

Secondly from a pragmatic sense, you have two, and ONLY two camps to choose from in this debate if we are talking about Von Neumann machines:

1) Subsequent problems with error in OS kernel execution is something that the hardware must protect against, and so must the formalized logic of the execution of the kernel.

or this camp, which is where I am in:

2) OS kernel problems with error in execution is a tools and engineering problem. The OS should remain simple for hardware as much as possible.

It should be clear why #2 is superior in cost, engineering and portability to the simplest hardware designs from pacemakers to the worlds largest super computers.

They all run one operating system, one MONOLITHIC OS KERNEL, and it isLINUX.
(Those that do not, are quaint.)

You will NEVER product a Micokernel that can straddle cost, performance and engineering as a result of #2.

And no hardware manufacturer would dare risk their balance sheets betting against Goedel's theorem.

End of Discussion and stay away from MicroKernels on Von Neumann machines.

-Hack

Reply Parent Score: 0

RE[6]: Comment by twitterfire
by Vanders on Thu 23rd Jan 2014 01:01 in reply to "RE[5]: Comment by twitterfire"
Vanders Member since:
2005-07-06

Well thanks for that fascinating digression into your mental health.

Reply Parent Score: 3

RE[6]: Comment by twitterfire
by ingraham on Thu 23rd Jan 2014 02:17 in reply to "RE[5]: Comment by twitterfire"
ingraham Member since:
2006-05-20

Because it is stupid?


I don't see how letting the user-space directly map L1 cache for IPC has anything to do with the rest of your diatribe.

...without anything going anywhere and no research to show for it.


As others have pointed out, there are numerous examples of successful microkernel OSes. Also, you've jumbled the "provably correct" issue and the micro- vs. monolithic- kernel debates.

You cannot define a system of logic that is not capable of self contradiction.


I'm reminded of that scene in Good Will Hunting:

Yeah, I read that too. Were you gonna plagiarize the whole thing for us? Do you have any thoughts of your own on this matter? Or do you, is that your thing, you come into a bar, read some obscure passage and then pretend - you pawn it off as your own, as your own idea just to impress some girls?


Side note: It's tsetse fly.

...you have two, and ONLY two camps to choose from...


Since we're bringing out our college class cheat sheets, I'll declare this to be an example of the Fallacy of the Excluded Middle. And, in fact, I can point out at least one other option. The NX bit / Data Execution Prevention is implemented both in hardware and software.



They all run one operating system, one MONOLITHIC OS KERNEL, and it is LINUX. (Those that do not, are quaint.)


That's a demonstrably false position. Consider page 42 of UBM's 2013 Embedded Market Study http://www.eetimes.com/document.asp?doc_id=1263083 (or http://e.ubmelectronics.com/2013EmbeddedStudy/index.html if you want the original, which is free but requires registration.) And that's not counting all the little embedded devices that have no actual OS.

You are right about supercomputers, of course. Still, the fact that Linux has a 95%+ share in that space doesn't mean it's completely perfect and there's no reason to every try anything else ever again. It's GOOD, yes. It's not the Answer to Life, the Universe, and Everything.

You will NEVER product a Micokernel that can straddle cost, performance and engineering as a result of #2.


Odd; I would think that a microkernel would be BETTER for point #2. Find a security flaw in a module? Fix it! On the fly without a reboot!

And no hardware manufacturer would dare risk their balance sheets betting against Goedel's theorem.


Except for Intel. And AMD. And ARM, DEC, Sun, IBM, Motorola...
http://en.wikipedia.org/wiki/NX_bit#Hardware_background

End of Discussion and stay away from MicroKernels on Von Neumann machines.


Even if I buy your premise (I don't) that Gödel's incompleteness theorem implies that there's no point to trying to formally prove correctness of software, I fail to see how that has anything to do with microkernel vs. monolithic. Your argument goes something like "Relativity proves we can't go faster than light, therefore steak is better than hamburger."

-James

Reply Parent Score: 3

RE[6]: Comment by twitterfire
by galvanash on Thu 23rd Jan 2014 02:19 in reply to "RE[5]: Comment by twitterfire"
galvanash Member since:
2006-01-25

Considering vander was asking about a hardware feature, I find your post both asinine and completely misdirected...

I'm just a web developer who reads way too much and is fascinated by the history of kernel design. The little I really know on the subject was read, I never did anything amounting to real kernel design, so my opinion on such matters is really worth squat - I just contribute where I think something I read is relevant.

Vander has actually done kernel design. From the tone and content of your post I doubt you could say the same... Linux is great. I like it, but it doesn't represent the final solution to system design for the rest of time...

Grow the fuck up.

Reply Parent Score: 3

RE[7]: Comment by twitterfire
by hackus on Thu 23rd Jan 2014 10:48 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