Skip to main content
USENIX
  • Conferences
  • Students
Sign in
  • Overview
  • Workshop Organizers
  • Workshop Program
  • Co-located Workshops
  • Activities
  • Sponsorship
  • Students and Grants
  • Questions?
  • Help Promote!
  • For Participants
  • Call for Papers
  • Past Workshops

twitter

Tweets by @usenix

usenix conference policies

  • Event Code of Conduct
  • Conference Network Policy
  • Statement on Environmental Responsibility Policy

You are here

Home » Leveraging Trusted Computing and Model Checking to Build Dependable Virtual Machines
Tweet

connect with us

http://twitter.com/usenix
http://www.usenix.org/facebook
http://www.usenix.org/linkedin
http://www.usenix.org/gplus
http://www.usenix.org/youtube

Leveraging Trusted Computing and Model Checking to Build Dependable Virtual Machines

Authors: 

Nuno Santos, INESC-ID and Instituto Superior Técnico, Universidade de Lisboa; Nuno P. Lopes, INESC-ID and Instituto Superior Técnico, Universidade de Lisboa and Microsoft Research

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.

Nuno Santos, INESC-ID and Instituto Superior Técnico, Universidade de Lisboa

Nuno P. Lopes, INESC-ID and Instituto Superior Técnico, Universidade de Lisboa and Microsoft Research

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {187152,
author = {Nuno Santos and Nuno P. Lopes},
title = {Leveraging Trusted Computing and Model Checking to Build Dependable Virtual Machines},
booktitle = {10th Workshop on Hot Topics in System Dependability (HotDep 14)},
year = {2014},
address = {Broomfield, CO},
url = {https://www.usenix.org/conference/hotdep14/workshop-program/presentation/santos},
publisher = {USENIX Association},
month = oct,
}
Download
Santos PDF
View the slides
  • Log in or    Register to post comments

© USENIX

  • Privacy Policy
  • Contact Us