Muen Kernel: Trustworthy by Design – Correct By Construction

http://www.muen.sk/

by jervisfm • 12 years ago

74 14 12 years ago

fab13n• 12 years ago

Honest question: who has a use-case for which a Raspberry wasn't powerful enough, but a Banana would have been?

Given that the Banana is about twice as expensive, here's a subsidiary question: who has a use-case for which TWO Raspberries wouldn't have been powerful enough, but a Banana would have been?

robinh• 12 years ago

I think you accidentally commented in the wrong thread. Gave me a hearty chuckle in this context, though.

Zenst• 12 years ago

Me too, just came from that Raspberry PI thread and thought, oh no my browser has corupted. Good chuckle.

aetherspawn• 12 years ago

Signed up just to comment on this. I've been wanting to do something similar for a while now (although, an exokernel).

You should update your source to use the new 2014 tools. The verifications become part of the syntax.

zobzu• 12 years ago

yeah verifications part of the code syntax seems like a decent concept for such cases

leccine• 12 years ago

This is amazing. I wish a company would build a minimalistic mobile platform on this without any support for social media. :)

hga2• 12 years ago

Hmmm, one problem I see with this, at least for us open source mortals, is that all this rigor sits atop a festering pile of C, that is, the GCC (the GNAT Ada compiler in it)....

At least as these people are using SPARK/Ada.

Then again, maybe I should return to looking at Intel CPU and chipset errata....

On the third hand, these guys aren't using systems with ECC.... (http://ark.intel.com/products/64893/intel-core-i7-3520m-proc...).

read• 12 years ago

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.

I had the impression seL4 was the first microkernel formally proven to be secure.

mokus• 12 years ago

Is seL4 open-source? Last time I looked, it wasn't.

Someone• 12 years ago

SeL4, AFAIK, isn't Open Source. You can only download binaries (http://ssrg.nicta.com.au/software/TS/seL4/)

Also, no runtime errors is quite different from secure, and at the source code level (which I think applies to both OSes) leaves room for compiler, linker, or standard library to introduce issues.

pavpanchekha• 12 years ago

It's my recollection that seL4 was proven correct at the binary level.

ballard• 12 years ago

For embedded/industrial applications the future is in domain-specific operating systems that are JEOS by virtue of not compling unneeded syscalls. OSes like Linux have way too many ABIs and internal machinery that just aren't necessary for headless systems and merely opens a huge attack surface by default... Even with make menuconfig stripped .config, there's still a ton of extra bells and whistles.

In a positive direction, it would be nice to be able to be able to strip out more functionality and still produce a functional kernel. Unfortunately, I don't think this is scalable with autotools or any configuration management setups without having more #ifdefs than code. Haskell could be a good candidate for such a kernel framework, but I'm sure there are other functional and imperative languages that have better complex configuration mgmt support with formal verification.

hga2• 12 years ago

Recently I've been thinking we need a "Device Driver Linux" distribution which can sit off to the side in systems like this or Xen, and just provide access to devices through careful external channels (although there's things like NFS you might want to use...).

The attack surface will still be huge, but perhaps by such hiding you can make it too hard for an attacker to actually get to it.

Muen Kernel: Trustworthy by Design – Correct By Construction

Related Stories