License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2013.45
URN: urn:nbn:de:0030-drops-46254
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4625/
Go to the corresponding LIPIcs Volume Portal

Barthe, Gilles ; Betarte, Gustavo ; Campo, Juan Diego ; Chimento, Jesús Mauricio ; Luna, Carlos

Formally Verified Implementation of an Idealized Model of Virtualization

pdf-format:
4.pdf (0.5 MB)

Abstract

VirtualCert is a machine-checked model of virtualization that can be
used to reason about isolation between operating systems in presence
of cache-based side-channels. In contrast to most prominent projects
on operating systems verification, where such guarantees are proved
directly on concrete implementations of hypervisors, VirtualCert
abstracts away most implementations issues and specifies the effects
of hypervisor actions axiomatically, in terms of preconditions and
postconditions. Unfortunately, seemingly innocuous implementation
issues are often relevant for security. Incorporating the treatment of
errors into VirtualCert is therefore an important step towards
strengthening the isolation theorems proved in earlier work. In this
paper, we extend our earlier model with errors, and prove that
isolation theorems still apply. In addition, we provide an executable specification of the hypervisor, and prove that it correctly implements the axiomatic model. The executable specification constitutes a first step towards a more realistic implementation of a hypervisor, and provides a useful tool for validating the axiomatic semantics developed in previous work.

BibTeX - Entry

@InProceedings{barthe_et_al:LIPIcs:2014:4625,
  author =	{Gilles Barthe and Gustavo Betarte and Juan Diego Campo and Jes{\'u}s Mauricio Chimento and Carlos Luna},
  title =	{{Formally Verified Implementation of an Idealized Model of Virtualization}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{45--63},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Ralph Matthes and Aleksy Schubert},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4625},
  URN =		{urn:nbn:de:0030-drops-46254},
  doi =		{10.4230/LIPIcs.TYPES.2013.45},
  annote =	{Keywords: virtualization, Cache and TLB, Executable specification, Error management, Isolation}
}

Keywords: virtualization, Cache and TLB, Executable specification, Error management, Isolation
Collection: 19th International Conference on Types for Proofs and Programs (TYPES 2013)
Issue Date: 2014
Date of publication: 25.07.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI