Paper Info
Title
Formally Verified System Initialisation.
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 engineering process. In this paper we present an automatic and formally verified initialiser for component-based systems built on the general-purpose microkernel seL4. The construction principles of this tool apply to capability systems in general and the proof ideas are not specific to 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 model 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 does not only provide automation, but also unprecedented assurance for reaching a desired system state. In addition to the engineering advantages, this result is a key prerequisite for reasoning about system-wide security and safety properties.
Year
DOI
Venue
2013
10.1007/978-3-642-41202-8_6
Lecture Notes in Computer Science
Keywords
Field
DocType
System Initialisation,seL4,Isabelle
HOL,Programming language,Computer science,Automated theorem proving,Microkernel,Communication channel,Theoretical computer science,Formal description,Software system,Automation,Engineering design process
Conference
Volume
ISSN
Citations 
8144
0302-9743
5
PageRank 
References 
Authors
0.44
12
9
Name
Order
Citations
PageRank
Andrew Boyton1192.33
June Andronick290342.66
Callum Bannister350.78
Matthew Fernandez4152.39
Xin Gao550.44
David Greenaway6141.01
Gerwin Klein7145087.47
Corey Lewis8333.30
Thomas Sewell991437.60