From a proven correct microkernel to trustworthy large systems

Select |




Print


Andronick, June

Andronick, June


2010-12-20


Conference Material


International Conference on Formal Verification of Object-Oriented Software


Paris


1-9


The seL4 microkernel was the world's first general-purpose operating system kernel with a formal, machine-checked proof of correctness. The next big step in the challenge of building truly trustworthy systems is to provide a framework for developing secure systems on top of seL4. This paper first gives an overview of seL4's correctness proof, together with its main implications and assumptions, and then describes our approach to provide formal security guarantees for large, complex systems.


LNCS


http://foveoos2010.cost-ic0701.org


The original publication is available at www.springerlink.com


nicta:4002


Andronick, June. From a proven correct microkernel to trustworthy large systems. In: Bernhard Beckert and Claude Marché Editor, editor/s. International Conference on Formal Verification of Object-Oriented Software; Paris. LNCS; 2010-12-20. 1-9.



Loading citation data...

Citation counts
(Requires subscription to view)