NICTA

file

Visible to the public Above and Beyond: seL4 Noninterference and Binary Verification (PT. 1)

Submitted by TimTh on Tue, 05/28/2013 - 12:12pm. Contributors:

ABSTRACT:

In 2009, the L4.verified project completed the world's first verification of functional correctness for a general-purpose OS kernel [2], seL4. Functional correctness here was embodied by a formal theorem of refinement, which stated that the behavior of the C code that implemented the kernel accorded with an abstract specification of how the kernel was meant to function.

file

Visible to the public 3 Years After L.4 Verified

Submitted by TimTh on Tue, 05/08/2012 - 9:53pm. Contributor:

Presented as part of the 2012 HCSS conference.

file

Visible to the public Verifying a High-Performance Micro-kernel

Submitted by TimTh on Thu, 02/02/2012 - 10:49am. Contributor:

Presented as part of the 2007 HCSS conference.

Abstract