The L4.verified Project - Next Steps

Gerwin Klein

Abstract

Last year, the NICTA L4.verified project produced a formal machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This paper gives a brief overview of the proof together with its main implications and assumptions, and paints a vision on how this verified kernel can be used for gaining assurance of overall system security on the code level for systems of a million lines of code or more.

This paper is an extended abstract for an invited talk at VSTTE 2010.

Online Copy

Extended abstract available as [PDF]

Bibtex entry

@InProceedings{Klein_10b,
    author =    {Gerwin Klein},
    title =     {The L4.verified Project - Next Steps},
    booktitle = {Proc.\ 3rd International Conference on Verified Software: Theories, Tools, Experiments (VSTTE'2010)},
    editor =    {Gary Leavens and Peter O'Hearn and Sriram Rajamani},
    year =      {2010},
    address =   {Edinburgh, UK},
    pages =     {86--96},
    month =     Aug,
    series =    {Lecture Notes in Computer Science},
    volume =    {6217},
    publisher =  {Springer},
}
Gerwin Klein
2010-08-20