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.
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

		Andrew Boyton Secure architectures on a verified microkernel PhD Thesis, CSE, UNSW, Sydney, Australia, November, 2014
		Andrew Boyton, June Andronick, Callum Bannister, Matthew Fernandez, Xin Gao, David Greenaway, Gerwin Klein, Corey Lewis and Thomas Sewell Formally verified system initialisation International Conference on Formal Engineering Methods, pp. 70–85, Queenstown, New Zealand, October, 2013
		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