Skip to main content

A formally verified OS kernel. now what?

Authors

Gerwin Klein

NICTA

UNSW

Abstract

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.

BibTeX Entry

  @inproceedings{Klein_10_1,
    isbn             = {3-642-14051-3},
    publisher        = {Springer},
    booktitle        = {International Conference on Interactive Theorem Proving},
    month            = jul,
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/3844.pdf},
    year             = {2010},
    editor           = {{M. Kaufmann and L. Paulson}},
    keywords         = {isabelle/hol, sel4},
    title            = {A Formally Verified {OS} Kernel. Now What?},
    author           = {Klein, Gerwin},
    address          = {Edinburgh, UK},
    pages            = {1--7}
  }

Download