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.