Leveraging Trusted Computing and Model Checking to Build Dependable Virtual Machines

In the last years, it has emerged a market of virtual ap-pliances, i.e., virtual machine images specifically con-figured 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, mis-configurations, privacy loss, etc. In this paper, we pro-pose 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 pro-vides for the automatic verification of the software’s high-level configuration properties. We present our ap-proach, and discuss open research challenges.