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.
To read all comments associated with this story, please click here.
Member since:
2006-05-20
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.
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.
I'm reminded of that scene in Good Will Hunting:
Side note: It's tsetse fly.
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.
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.
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!
Except for Intel. And AMD. And ARM, DEC, Sun, IBM, Motorola...
http://en.wikipedia.org/wiki/NX_bit#Hardware_background
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