Skip to main content

System initialisation

A goal of our Trusted Components project is to provide Verified system initialisation.

  • Aim: Produce a user-level system initialisation component that starts the threads of a seL4 system as per a formal specification in a verified manner.

    Sys init
  • Overview: All of the existing seL4 proofs, such as information flow, rely on the system being first set up correctly. If it is not, components that should be isolated might not be, or they might not have access to the hardware they should have access to.

    For large, complex systems, getting this correct can be hard. Many embedded systems have custom, low-level, hand-crafted code to carry out this task, but due to the low-level and precise nature of this code, getting it right is both tricky and important.

    This project aims to create a single user-level system-initialisation component that takes a formal specification and is formally verified to initialise the user-level system into this given state. We aim to produce a formal model of this component and prove the correctness of both this model, and its C implementation.

  • Technical research challenges:

    • Model the functions of a user-level initialisation component.
    • Reason about user-level code using the guarantees proven about seL4.
    • Prove simple separation-logic style semantics of the seL4 API from the user-level.
    • Refine user-level code running on seL4.

Publications

Abstract PDF Andrew Boyton
Secure architectures on a verified microkernel
PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014
Abstract
Slides
PDF Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis and Thomas Sewell
Formally verified system initialisation
Proceedings of the 15th International Conference on Formal Engineering Methods, pp. 70–85, Queenstown, New Zealand, October, 2013
Abstract PDF June Andronick, Andrew Boyton and Gerwin Klein
Final report for AOARD grant #FA2386-11-1-4070, formal system verification — extension
Technical Report, NICTA, October, 2012

People


Served by Apache on Linux on seL4.