Skip to Main content Skip to Navigation
New interface
Conference papers

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 metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Thomas Jensen Connect in order to contact the contributor
Submitted on : Tuesday, November 8, 2016 - 6:10:00 PM
Last modification on : Saturday, June 25, 2022 - 7:39:57 PM


Files produced by the author(s)



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⟩



Record views


Files downloads