Muen Kernel: Trustworthy by Design – Correct By Construction

Signed up just to comment on this. I&#x27;ve been wanting to do something similar for a while now (although, an exokernel).<p>You should update your source to use the new 2014 tools. The verifications become part of the syntax.

For embedded&#x2F;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&#x27;t necessary for headless systems and merely opens a huge attack surface by default... Even with make menuconfig stripped .config, there&#x27;s still a ton of extra bells and whistles.<p>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&#x27;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&#x27;m sure there are other functional and imperative languages that have better complex configuration mgmt support with formal verification.

Honest question: who has a use-case for which a Raspberry wasn&#x27;t powerful enough, but a Banana would have been?<p>Given that the Banana is about twice as expensive, here&#x27;s a subsidiary question: who has a use-case for which TWO Raspberries wouldn&#x27;t have been powerful enough, but a Banana would have been?

&gt; 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.<p>I had the impression seL4 was the first microkernel formally proven to be secure.

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)....<p>At least as these people are using SPARK&#x2F;Ada.<p>Then again, maybe I should return to looking at Intel CPU and chipset errata....<p>On the third hand, these guys aren&#x27;t using systems with ECC.... (<a href="http://ark.intel.com/products/64893/intel-core-i7-3520m-processor-4m-cache-up-to-3_60-ghz" rel="nofollow">http:&#x2F;&#x2F;ark.intel.com&#x2F;products&#x2F;64893&#x2F;intel-core-i7-3520m-proc...</a>).

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