Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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



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.


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.


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




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: