Formally Verified System Initialisation

Select |




Print


Boyton, Andrew; Andronick, June; Bannister, Callum; Fernandez, Matthew; Gao, Xin; Greenaway, David; Klein, Gerwin; Lewis, Corey; Sewell, Thomas

Boyton, Andrew; Andronick, June; Bannister, Callum; Fernandez, Matthew; Gao, Xin; Greenaway, David; Klein, Gerwin; Lewis, Corey; Sewell, Thomas


2013-10-29


Conference Material


15th International Conference on Formal Engineering Methods (ICFEM 2013)


Queenstown, New Zealand


70-85


The safety and security of software systems depends heavily on how they are initially configured. Manually writing program code that establishes such an initial configuration is a tedious and error-prone engineering process. In this paper we present our automatic and formally verified initialiser for component-based systems 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 access rights. We provide a formal specification of the initialiser and prove, in the theorem prover Isabelle/HOL, that the resulting state is the desired one. Our proof formally connects to the existing functional correctness proof of the seL4 microkernel. This tool not only automates the process of initialising a system, it also provides unprecedented assurance for reaching a desired safe system state. In addition to the engineering advantages, this result is a key prerequisite for reasoning about system-wide security and safety properties.


Springer


System Initialisation, seL4, Isabelle


https://doi.org/10.1007/978-3-642-41202-8_6


https://www.cs.auckland.ac.nz/research/conferences/icfem2013/


nicta:7047


Boyton, Andrew; Andronick, June; Bannister, Callum; Fernandez, Matthew; Gao, Xin; Greenaway, David; Klein, Gerwin; Lewis, Corey; Sewell, Thomas. Formally Verified System Initialisation. In: Lindsay Groves, Jing Sun Editor, editor/s. 15th International Conference on Formal Engineering Methods (ICFEM 2013); Queenstown, New Zealand. Springer; 2013-10-29. 70-85. https://doi.org/10.1007/978-3-642-41202-8_6



Loading citation data...

Citation counts
(Requires subscription to view)