Formal Verification of Secure User Mode Device Execution with DMA
Number of Authors: 2
2014 (English)Conference paper (Refereed)
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.
peripheral devices, DMA, separation, isolation, user mode execution, ARM, formal hardware/software co-verification, theorem proving, HOL4
Computer and Information Science
IdentifiersURN: urn:nbn:se:ri:diva-15561OAI: oai:DiVA.org:ri-15561DiVA: diva2:1036878
Haifa Verification Conference
ProjectsProvably 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 http://link.springer.com/10.1007/978-3-319-13338-6_18.2016-10-132016-10-13