Trustworthy Systems

Secure architectures on a verified microkernel

Authors

Andrew Boyton

NICTA

UNSW

Abstract

The safety and security of software systems depends on how they are initially configured. Manually writing program code that establishes such an initial configuration is a tedious and error-prone process, and yet most systems now are initialised with manually written, ad-hoc code. This thesis provides a solution to this process, presenting an automatic and formally verified system initialiser for component-based systems built on the general-purpose microkernel seL4. The initialiser takes a declarative formal description of the desired initialised state, and uses seL4-provided services to create all necessary components, setup their communication channels, and distribute the required capabilities. We analyse a model for capability-based systems, namely the take-grant protection model, and extend the existing literature to develop a formal model in Isabelle/HOL that models real-world capability-based systems such as seL4 more accurately. We use this to demonstrate how the security of a system can be conferred by capabilities. We provide a formal algorithm of system initialisation and prove, in the theorem prover Isabelle/HOL, that the resulting state conforms with the desired one, giving us an unprecedented level of assurance for the correctness of system initialisation. Our proof formally connects to the existing functional correctness proof of the seL4 microkernel. In the process of this work, we develop a custom separation algebra, with a fine-level of granularity, for reasoning about both the API of the seL4 microkernel and the user-level code running on seL4.

BibTeX Entry

  @phdthesis{Boyton:phd,
    address          = {Sydney, Australia},
    author           = {Boyton, Andrew},
    month            = nov,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/9141.pdf},
    school           = {CSE, UNSW},
    title            = {Secure architectures on a verified microkernel},
    year             = {2014}
  }

Download