Trustworthy Systems

Proof engineering considered essential

Authors

Gerwin Klein

NICTA

UNSW

Abstract

In this talk, I will give an overview of the various formal verification projects around the evolving seL4 microkernel, and discuss our experience in large-scale proof engineering and maintenance.

In particular, the presentation will draw a picture of what these verifications mean and how they fit together into a whole. Among these are a number of firsts: the first code-level functional correctness proof of a general-purpose OS kernel, the first non-interference proof for such a kernel at the code-level, the first binary-level functional verification of systems code of this complexity, and the first sound worst-case execution-time profile for a protected-mode operating system kernel.

Taken together, these projects produced proof artefacts on the order of 400,000 lines of Isabelle/HOL proof scripts. This order of magnitude brings engineering aspects to proofs that we so far mostly associate with software and code. In the second part of the talk, I will report on our experience in proof engineering methods and tools, and pose a number of research questions that we think will be important to solve for the wider scale practical application of such formal methods in industry.

BibTeX Entry

  @inproceedings{Klein_14,
    address          = {Singapore},
    author           = {Klein, Gerwin},
    booktitle        = {International Symposium on Formal Methods (FM)},
    doi              = {10.1007/978-3-319-06410-9_2},
    editor           = {{Cliff Jones, Pekka Pihlajasaari, Jun Sun}},
    keywords         = {proof engineering, sel4, isabelle/hol},
    month            = apr,
    pages            = {16--21},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/7923.pdf},
    publisher        = {Springer},
    slides           = {https://trustworthy.systems/publications/nicta_slides/7923.pdf},
    title            = {Proof Engineering Considered Essential},
    year             = {2014}
  }

Download