Change search
ReferencesLink to record
Permanent link

Direct link
Formal Verification of Secure User Mode Device Execution with DMA
Provably Secure Execution Platforms for Embedded Systems.
Number of Authors: 2
2014 (English)Conference paper (Refereed)
Abstract [en]

Separation between processes on top of an operating system or between guests in a virtualized environment is essential for establishing security on modern platforms. A key requirement of the underlying hardware is the ability to support multiple partitions executing on the shared hardware without undue interference. For modern processor architectures - with hardware support for memory management, several modes of operation and I/O interfaces - this is a delicate issue requiring deep analysis at both instruction set and processor implementation level. In a first attempt to rigorously answer this type of questions we introduced in previous work an information flow analysis of user program execution on an ARMv7 platform with hardware supported memory protection, but without I/O. The analysis was performed as a semi-automatic proof search procedure on top of an ARMv7 ISA model implemented in the Cambridge HOL4 theorem prover by Fox et al. The restricted platform functionality, however, makes the analysis of limited practical value. In this paper we add support for devices, including DMA, to the analysis. To this end, we propose an approach to device modeling based on the idea of executing devices nondeterministically in parallel with the (single-core) deterministic processor, covering a fine granularity of interactions between the model components. Based on this model and taking the ARMv7 ISA as an example, we provide HOL4 proofs of several noninterference-oriented isolation properties for a partition executing in the presence of devices which potentially use DMA or interrupts.

Place, publisher, year, edition, pages
2014, 9. 236-251 p.
Keyword [en]
peripheral devices, DMA, separation, isolation, user mode execution, ARM, formal hardware/software co-verification, theorem proving, HOL4
National Category
Computer and Information Science
URN: urn:nbn:se:ri:diva-24374OAI: diva2:1043455
Haifa Verification Conference
Provably Secure Execution Platforms for Embedded Systems
This is the author version of the correspondent paper published in “Hardware and Software: Verification and Testing”, the proceedings of HVC 2014 (editor: Eran Yahav), Springer LNCS 8855. The publisher is Springer International Publishing Switzerland. The final publication is available at from: 2016-10-31 Created: 2016-10-31

Open Access in DiVA

fulltext(504 kB)4 downloads
File information
File name FULLTEXT01.pdfFile size 504 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Other links

By organisation
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 4 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

Total: 11 hits
ReferencesLink to record
Permanent link

Direct link