TUM Logo

A Formal Model for Virtual Machine Introspection

Virtual machine introspection (VMI) describes the method of monitoring and analyzing the state of a virtual machine from the hypervisor level. In this paper, we present a formal discussion of the development of VMI-based security appli- cations. We begin by identifying three major challenges that all VMI-based security applications must overcome. The main contribution of our work is the definition of a formal model for describing VMI techniques. This model is broken down in such a way that allows for thorough discussion of any VMI approach with regard to each of the three chal- lenges. Then, we specify three design patterns for interpret- ing state information using our model. We argue that these patterns are complete, that is, they cover all possible meth- ods for state interpretation. The properties of all patterns are thoroughly discussed so that the pros and cons of their application may be fully understood. Finally, we describe and discuss an ideal VMI-based intrusion detection system using our model and begin to detail the practical implica- tions in building such a system.

A Formal Model for Virtual Machine Introspection

Proceedings of the 2nd Workshop on Virtual Machine Security (VMSec '09)

Authors: Jonas Pfoh, Christian Schneider, and Claudia Eckert
Year/month: 2009/11
Booktitle: Proceedings of the 2nd Workshop on Virtual Machine Security (VMSec '09)
Pages: 1--10
Address: Chicago, Illinois, USA
Publisher: ACM Press
Fulltext: PfohSchneider2009a.pdf

Abstract

Virtual machine introspection (VMI) describes the method of monitoring and analyzing the state of a virtual machine from the hypervisor level. In this paper, we present a formal discussion of the development of VMI-based security appli- cations. We begin by identifying three major challenges that all VMI-based security applications must overcome. The main contribution of our work is the definition of a formal model for describing VMI techniques. This model is broken down in such a way that allows for thorough discussion of any VMI approach with regard to each of the three chal- lenges. Then, we specify three design patterns for interpret- ing state information using our model. We argue that these patterns are complete, that is, they cover all possible meth- ods for state interpretation. The properties of all patterns are thoroughly discussed so that the pros and cons of their application may be fully understood. Finally, we describe and discuss an ideal VMI-based intrusion detection system using our model and begin to detail the practical implica- tions in building such a system.

Bibtex:

@inproceedings { PfohSchneider2009a,
author = { Jonas Pfoh and Christian Schneider and Claudia Eckert},
title = { A Formal Model for Virtual Machine Introspection },
year = { 2009 },
month = { November },
booktitle = { Proceedings of the 2nd Workshop on Virtual Machine Security (VMSec '09) },
address = { Chicago, Illinois, USA },
pages = { 1--10 },
publisher = { ACM Press },
url = {https://www.sec.in.tum.de/i20/publications/a-formal-model-for-virtual-machine-introspection/@@download/file/PfohSchneider2009a.pdf}
}