Leveraging Trusted Computing and Model Checking to Build Dependable Virtual Machines

Nuno Santos and Nuno P. Lopes

 

Abstract:

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.

 

Published:

N. Santos and N. P. Lopes. Leveraging Trusted Computing and Model Checking to Build Dependable Virtual Machines. In Proc. of the 10th Workshop on Hot Topics in System Dependability (HotDep), Oct. 2014.

 

Download:

 

Bibtex:

@inproceedings{depliance-hotdep14,
  title =	{Leveraging Trusted Computing and Model Checking to Build Dependable Virtual Machines},
  author =	{Nuno Santos and Nuno P. Lopes},
  booktitle =	{Proc. of the 10th Workshop on Hot Topics in System Dependability (HotDep)},
  month =	oct,
  year =	2014
}

<-- Return