From a Verified Kernel towards Verified Systems

Gerwin Klein

Abstract

The L4.verified project has produced a formal, machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This paper briefly summarises the proof, its main implications and assumptions, reports on the experience in conducting such a large-scale verification, and finally lays out a vision how this formally verified kernel may be used for gaining formal, code-level assurance about safety and security properties of systems on the order of a million lines of code.

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

Online Copy

Extended abstract available as [PDF]

Bibtex entry

@InProceedings{Klein_10c,
    author =    {Gerwin Klein},
    title =     {From a Verified Kernel towards Verified Systems},
    booktitle = {Proc.\ 8th Asian Symposium on Programming Languages and Systems (APLAS 2010)},
    editor =    {Kazunori Ueda},
    year =      {2010},
    address =   {Shanghai, China},
    pages =     {21--33},
    month =     Nov,
    series =    {Lecture Notes in Computer Science},
    volume =    {6461},
    publisher =  {Springer},
}
Gerwin Klein
2010-11-29