Modeling and Abstraction of Memory Management in a Hypervisor

Pauline Bolignano 1 Thomas Jensen 1 Vincent Siles 2
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Hypervisors must isolate memories of guest operating systems. This paper is concerned with proving memory isolation properties about the virtualization of the memory management unit provided by a hypervisor through shadow page tables. We conduct the proofs using abstraction techniques between high-level and low-level descriptions of the system, based on techniques from previous work on formally proving memory isolation in micro-kernels. The present paper shows how a hypervisor developed by Technische Universität Berlin has been formalized and presents the isolation properties we have proved on the targeted abstract model. In particular, we provide details about how the management of page tables has been formally modeled.
Document type :
Conference papers
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-01394174
Contributor : Thomas Jensen <>
Submitted on : Tuesday, November 8, 2016 - 6:10:00 PM
Last modification on : Thursday, February 7, 2019 - 3:46:45 PM

File

HypFASE.pdf
Files produced by the author(s)

Identifiers

Citation

Pauline Bolignano, Thomas Jensen, Vincent Siles. Modeling and Abstraction of Memory Management in a Hypervisor. Fundamental Approaches to Software Engineering (FASE’16), Apr 2016, Eindhoven, Netherlands. pp.214 - 230, ⟨10.1007/978-3-662-49665-7_13⟩. ⟨hal-01394174⟩

Share

Metrics

Record views

1427

Files downloads

140