Automatic Derivation of Platform Noninterference Properties
2016 (English)In: Software Engineering and Formal Methods, Springer LNCS 9763 / [ed] Rocco De Nicola, Eva Kühn, 2016, 27-44 p.Conference paper (Refereed)
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 computingbase, 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.
Place, publisher, year, edition, pages
2016. 27-44 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 9763
Instruction set architectures, ARM, MIPS, noninterference, information flow, theorem proving, HOL4
Research subject Computer Science
IdentifiersURN: urn:nbn:se:kth:diva-192451DOI: 10.1007/978-3-319-41591-8_3ISBN: 978-3-319-41590-1ISBN: 978-3-319-41591-8OAI: oai:DiVA.org:kth-192451DiVA: diva2:968447
Software Engineering and Formal Methods (SEFM)
FunderVINNOVASwedish Foundation for Strategic Research Swedish Civil Contingencies Agency
QC 201609162016-09-122016-09-122016-09-16Bibliographically approved