Open Kernel Labs’ kernel proved correct

Posted by Ken Y-N on February 4th, 2010 at 02:46pm

L4 and its variants is a popular microkernel that can be found in many places, including even right at the bottom of Google’s Android system. So, I was interested to read about a formal proof for seL4, after five years of work by Open Kernel Labs and NICTA, Australia’s Information and Communications Technology Research Centre of Excellence, on 7,500 lines of code. Open Kernel Labs also have a White Paper on the subject available on their website.

Tags: open kernel labs, sel4

Under Virtualisation Tags: open kernel labs, sel4