Formal Verification of Secure User Mode Device Execution with DMA
2014 (English)In: Hardware and Software: Verification and Testing / [ed] Eran Yahav, Springer Publishing Company, 2014, 236-251 p.Conference paper (Refereed)
Separation between processes on top of an operating systemor between guests in a virtualized environment is essential for establish-ing security on modern platforms. A key requirement of the underlyinghardware is the ability to support multiple partitions executing on theshared hardware without undue interference. For modern processor archi-tectures - with hardware support for memory management, several modesof operation and I/O interfaces - this is a delicate issue requiring deepanalysis at both instruction set and processor implementation level. In afirst attempt to rigorously answer this type of questions we introducedin previous work an information flow analysis of user program executionon an ARMv7 platform with hardware supported memory protection,but without I/O. The analysis was performed as a semi-automatic proofsearch procedure on top of an ARMv7 ISA model implemented in theCambridge HOL4 theorem prover by Fox et al. The restricted platformfunctionality, however, makes the analysis of limited practical value. Inthis paper we add support for devices, including DMA, to the analy-sis. To this end, we propose an approach to device modeling based onthe idea of executing devices nondeterministically in parallel with the(single-core) deterministic processor, covering a fine granularity of inter-actions between the model components. Based on this model and tak-ing the ARMv7 ISA as an example, we provide HOL4 proofs of severalnoninterference-oriented isolation properties for a partition executing inthe presence of devices which potentially use DMA or interrupts.
Place, publisher, year, edition, pages
Springer Publishing Company, 2014. 236-251 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 8855
peripheral devices, DMA, separation, isolation, user mode execu- tion, ARM, formal hardware/software co-verification, theorem proving, HOL4
Research subject Computer Science
IdentifiersURN: urn:nbn:se:kth:diva-155718DOI: 10.1007/978-3-319-13338-6_18ScopusID: 2-s2.0-84921419001ISBN: 978-3-319-13337-9ISBN: 978-3-319-13338-6OAI: oai:DiVA.org:kth-155718DiVA: diva2:762165
10th International Haifa Verification Conference, HVC 2014
FunderSwedish Foundation for Strategic Research
QC 201411172014-11-102014-11-102016-09-12Bibliographically approved