Parametric verification of address space separation. (English) Zbl 1353.68177

Franklin, Jason; Chaki, Sagar; Datta, Anupam; McCune, Jonathan M.; Vasudevan, Amit

Degano, Pierpaolo (ed.) et al., Principles of security and trust. First international conference, POST 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28640-7/pbk). Lecture Notes in Computer Science 7215, 51-68 (2012).

Summary: The address translation subsystem of operating systems, hypervisors, and virtual machine monitors must correctly enforce address space separation in the presence of adversaries. The size, and hierarchical nesting, of the data structures over which such systems operate raise challenges for automated model checking techniques to be fruitfully applied to them. We address this problem by developing a sound and complete parametric verification technique that achieves the best possible reduction in model size. Our results significantly generalize prior work on this topic, and bring interesting systems within the scope of analysis. We demonstrate the applicability of our approach by modeling shadow paging mechanisms of Xen version 3.0.3 and ShadowVisor, a research hypervisor developed for the x86 platform.
For the entire collection see [Zbl 1238.68013].

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68N25	Theory of operating systems