Skip to main content

A formally verified OS kernel. now what?

Authors

Gerwin Klein

NICTA

UNSW

Abstract

We present an overview of the different refinement frameworks used in the L4.verified project to formally prove the functional correctnes of the seL4 microkernel. The verification is conducted in the interactive theorem prover Isabelle/HOL and proceeds in two large refinement steps: one proof between two monadic, functional specifications in HOL and one proof between such a monadic specification and a C program. To connect these proofs into one overall theorem, we map both refinement statements into a common overall framework.

BibTeX Entry

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

Download

Served by Apache on Linux on seL4.