3 ms·
> 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.
by read 12y 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 12y agoIs seL4 open-source? Last time I looked, it wasn't.
- Someone 12y agoSeL4, AFAIK, isn't Open Source. You can only download binaries (http://ssrg.nicta.com.au/software/TS/seL4/ 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 12y agoIt's my recollection that seL4 was proven correct at the binary level.
- pgeorgi 12y ago"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 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.