Formal Verification of Secure User Mode Device Execution with DMA

Schwarz, Oliver and Dam, Mads (2014) Formal Verification of Secure User Mode Device Execution with DMA. In: Haifa Verification Conference, Haifa, Israel.

PDF (author version) - Accepted Version

Official URL:


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.

Item Type:Conference or Workshop Item (Paper)
Additional Information: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
Uncontrolled Keywords:peripheral devices, DMA, separation, isolation, user mode execution, ARM, formal hardware/software co-verification, theorem proving, HOL4
ID Code:5745
Deposited By:Oliver Schwarz
Deposited On:11 Nov 2014 10:37
Last Modified:11 Nov 2014 10:37

Repository Staff Only: item control page