Change search
ReferencesLink to record
Permanent link

Direct link
Automatic Derivation of Platform Noninterference Properties
RISE, Swedish ICT, SICS. SEC.
PROSPER.
Number of Authors: 2
2016 (English)Conference paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
2016, 8.
Keyword [en]
Instruction set architectures, ARM, MIPS, noninterference, information flow, theorem proving, HOL4
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:ri:diva-24556DOI: 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_3OAI: oai:DiVA.org:ri-24556DiVA: diva2:1043641
Conference
Software Engineering and Formal Methods (SEFM)
Projects
PROSPERHASPOC
Note
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_3Available from: 2016-10-31 Created: 2016-10-31

Open Access in DiVA

fulltext(335 kB)6 downloads
File information
File name FULLTEXT01.pdfFile size 335 kBChecksum SHA-512
9b125ce3c3822207c86f012e88f1483f39a2c4ec77467cd55bcb8ddd7780cb9c4e2d162b63c0cb605089fc597b5edfc1bd36bf835192c3421c195def811e3993
Type fulltextMimetype application/pdf

Other links

Publisher's full texthttp
By organisation
SICS
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 6 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 17 hits
ReferencesLink to record
Permanent link

Direct link