Trustworthy virtualization of the ARMv7 memory subsystem
2015 (English)In: 41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015, Springer Berlin/Heidelberg, 2015, 578-589 p.Conference paper (Refereed)
In order to host a general purpose operating system, hypervisors need to virtualize the CPU memory subsystem. This entails dynamically changing MMU resources, in particular the page tables, to allow a hosted OS to reconfigure its own memory. In this paper we present the verification of the isolation properties of a hypervisor design that uses direct paging. This virtualization approach allows to host commodity Oss without requiring either shadow data structures or specialized hardware support. Our verification targets a system consisting of a commodity CPU for embedded devices (ARMv7), a hypervisor and an untrusted guest running Linux.The verification involves three steps: (i) Formalization of an ARMv7 CPU that includes the MMU, (ii) Formalization of a system behavior that includes the hypervisor and the untrusted guest (iii) Verification of the isolation properties. Formalization and proof are done in the HOL4 theorem prover, thus allowing to re-use the existing HOL4 ARMv7 model developed in Cambridge.
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2015. 578-589 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 8939
Formal verification, Hypervisor, Memory management, Theorem proving, Virtual reality, Embedded device, Memory subsystems, Specialized hardware, System behaviors, Theorem provers, Virtualizations, Memory management units
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-167389DOI: 10.1007/978-3-662-46078-8_48ISI: 000357679300047ScopusID: 2-s2.0-84922031791ISBN: 9783662460771OAI: oai:DiVA.org:kth-167389DiVA: diva2:815173
41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015; Pec pod Sněžkou; Czech Republic; 24 January 2015 through 29 January 2015
QC 201505292015-05-292015-05-222016-07-14Bibliographically approved