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
1 Comment for Open Kernel Labs’ kernel proved correct
1. State of the art in Secur&hellip | May 11th, 2010 at 2:44 pm
[...] European Union and the USA’s best are described in outline; to me the one of most interest is selL4, Secure L4, as it is a real product and is closely related to the OKL4 kernel that appears in such places as [...]
Leave a Comment for Open Kernel Labs’ kernel proved correct