Trustworthy Systems

Microkernel verification down to assembly

Authors

Matthew Fernandez, Gerwin Klein and Ihor Kuz

NICTA

UNSW

Published:

Poster presented at EuroSys 2012

Abstract

When constructing systems with high assurance requirements, it is desirable to build on a formally verified trusted computing base, such as the seL4 microkernel. The verification of seL4 guarantees correctness down to the kernel's C implementation and relies on the correctness of the C compiler used. CompCert, a verified C compiler, has the potential to extend these guarantees to the level of assembly. We have made significant modifications to seL4, which has previously only been compiled with variants of GCC, in order to make it compatible with CompCert. The poster proposed will discuss the challenges that have been encountered, some lessons learnt and what we hope to gain from this approach.

The contribution of this work is a first step towards our overall aim of the formal verification of a microkernel from a C implementation down to an assembly implementation. To our knowledge, this will be the first proof of functional correctness of a general-purpose operating system kernel down to assembly. The main achievement thus far is applying CompCert to seL4, during which we have already learnt some valuable lessons.

BibTeX Entry

  @misc{Fernandez_KK_12,
    address          = {Bern, Switzerland},
    author           = {Fernandez, Matthew and Klein, Gerwin and Kuz, Ihor},
    howpublished     = {Poster presented at EuroSys 2012},
    keywords         = {sel4, compcert, microkernel, formal verification},
    month            = apr,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/5857.pdf},
    title            = {Microkernel Verification Down To Assembly},
    year             = {2012}
  }

Download