Leveraging Trusted Computing and Model Checking to Build Dependable Virtual Machines

In the last years, it has emerged a market of virtual appliances, i.e., virtual machine images specifically configured to provide a given service (e.g., web hosting). The virtual appliance model greatly reduces the burden of configuring virtual machines from scratch. However, the current model involves risks: security threats, misconfigurations, privacy loss, etc. In this paper, we propose an approach to build dependable virtual machines. It is based on trusted computing and model checking: trusted computing allows for low-level attestation of the software of a virtual appliance, and model checking provides for the automatic verification of the software’s high-level configuration properties. We present our approach, and discuss open research challenges.