Muen Kernel: Trustworthy by Design – Correct By Construction(muen.sk)
muen.sk
Muen Kernel: Trustworthy by Design – Correct By Construction
http://www.muen.sk/
14 comments
yeah verifications part of the code syntax seems like a decent concept for such cases
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.
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.
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.
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.
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?
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?
> 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.
I had the impression seL4 was the first microkernel formally proven to be secure.
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.
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.
It's my recollection that seL4 was proven correct at the binary level.
"We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation." http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
Of course they might have improved on that later, this paper is ~5 years old now.
Of course they might have improved on that later, this paper is ~5 years old now.
Is seL4 open-source? Last time I looked, it wasn't.
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...).
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...).
This is amazing. I wish a company would build a minimalistic mobile platform on this without any support for social media. :)
You should update your source to use the new 2014 tools. The verifications become part of the syntax.