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.
Type de document :
Communication dans un congrès
Fundamental Approaches to Software Engineering (FASE’16), Apr 2016, Eindhoven, Netherlands. Springer, Springer LNCS 9633, pp.214 - 230, 2016, Proc. of Fundamental Approaches to Software Engineering (FASE’16). 〈10.1007/978-3-662-49665-7_13〉
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01394174
Contributeur : Thomas Jensen <>
Soumis le : mardi 8 novembre 2016 - 18:10:00
Dernière modification le : mercredi 16 mai 2018 - 11:23:28

Fichier

HypFASE.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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. Springer, Springer LNCS 9633, pp.214 - 230, 2016, Proc. of Fundamental Approaches to Software Engineering (FASE’16). 〈10.1007/978-3-662-49665-7_13〉. 〈hal-01394174〉

Partager

Métriques

Consultations de la notice

1055

Téléchargements de fichiers

78