from Hacker News

Muen Kernel: Trustworthy by Design – Correct By Construction

by jervisfm on 4/27/14, 7:04 PM with 14 comments

  • by aetherspawn on 4/27/14, 9:50 PM

    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.

  • by ballard on 4/28/14, 12:28 PM

    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.

  • by fab13n on 4/27/14, 9:21 PM

    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?

  • by read on 4/28/14, 2:47 AM

    > 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.

  • by hga on 4/28/14, 12:49 AM

    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...).

  • by leccine on 4/27/14, 10:50 PM

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