DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2013.45

Formally Verified Implementation of an Idealized Model of Virtualization

Authors: Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, and Carlos Luna

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

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.

Cite as

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, and Carlos Luna. Formally Verified Implementation of an Idealized Model of Virtualization. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 45-63, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{barthe_et_al:LIPIcs.TYPES.2013.45,
  author =	{Barthe, Gilles and Betarte, Gustavo and Campo, Juan Diego and Chimento, Jes\'{u}s Mauricio and Luna, Carlos},
  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 =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.45},
  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}
}

Search Results

Documents authored by Campo, Juan Diego

Formally Verified Implementation of an Idealized Model of Virtualization

Abstract

Cite as

Thanks for your feedback!

Could not send message