Schwarz, Oliver and Dam, Mads (2016) Automatic Derivation of Platform Noninterference Properties. In: Software Engineering and Formal Methods (SEFM).
|PDF (Preprint author version) - Accepted Version|
Official URL: http://dx.doi.org/10.1007/978-3-319-41591-8_3
For the verification of system software, information flow properties of the instruction set architecture (ISA) are essential. They show how information propagates through the processor, including sometimes opaque control registers. Thus, they can be used to guarantee that user processes cannot infer the state of privileged system components, such as secure partitions. Formal ISA models - for example for the HOL4 theorem prover - have been available for a number of years. However, little work has been published on the formal analysis of these models. In this paper, we present a general framework for proving information flow properties of a number of ISAs automatically, for example for ARM. The analysis is represented in HOL4 using a direct semantical embedding of noninterference, and does not use an explicit type system, in order to (i) minimize the trusted computing base, and to (ii) support a large degree of context-sensitivity, which is needed for the analysis. The framework determines automatically which system components are accessible at a given privilege level, guaranteeing both soundness and accuracy.
|Item Type:||Conference or Workshop Item (Paper)|
|Additional Information:||This is the author version of the correspondent paper published in "Software Engineering and Formal Methods", the proceedings of SEFM 2016 (editors: Rocco De Nicola, Eva Kühn), Springer LNCS 9763. The publisher is Springer International Publishing Switzerland. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-41591-8_3|
|Uncontrolled Keywords:||Instruction set architectures, ARM, MIPS, noninterference, information flow, theorem proving, HOL4|
|Deposited By:||Oliver Schwarz|
|Deposited On:||18 Aug 2016 15:01|
|Last Modified:||18 Aug 2016 15:01|
Repository Staff Only: item control page