Last year, the 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. In my presentation I will summarise the proof together with its main implications and assumptions, I will describe in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security, and I will explore further future research directions that open up with a formally verified OS kernel.

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

@InProceedings{Klein_10,
    author =    {Gerwin Klein},
    title =     {A Formally Verified OS Kernel. Now What?},
    booktitle = {Proc.\ First International Conference on Interactive Theorem Proving (ITP'2010)},
    editor =    {Matt Kaufmann and Lawrence C Paulson},
    year =      {2010},
    address =   {Edinburgh, UK},
    pages =     {1--7},
    month =     Jul,
    series =    {Lecture Notes in Computer Science},
    volume =    {6172},
    publisher =  {Springer},
}