Skip to main content

A formally verified OS kernel. Now what?


Gerwin Klein

NICTA, Sydney, Australia
UNSW, Australia

Invited extended 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

    author           = {Gerwin Klein},
    editor           = {Matt Kaufmann and Lawrence C Paulson},
    month            = jul,
    series           = {Lecture Notes in Computer Science},
    year             = {2010},
    title            = {A Formally Verified {OS} Kernel. {Now} What?},
    address          = {Edinburgh, UK},
    pages            = {1--7},
    volume           = {6172},
    booktitle        = {Proceedings of the 1st International Conference on Interactive Theorem Proving},
    publisher        = {Springer}


Served by Apache on Linux on seL4.