Skip to main content.
Advanced search >
<< Back to previous page Print

<< Tuesday, May 14, 2013 >>

Remind me

Tell a friend

Add to my Google calendar (bCal)

Download to my calendar

Bookmark and ShareShare

[Dissertation Talk] Secure Virtualization with Formal Methods

Seminar: Departmental | May 14 | 2-3 p.m. | 380 Soda Hall

Cynthia Sturton, University of California, Berkeley

Electrical Engineering and Computer Sciences (EECS)

Virtualization software is increasingly a part of the infrastructure behind our online activities. The companies and institutions that produce online content are taking advantage of the "infrastructure as a service" cloud computing model to obtain cheap and reliable computing power. These content producers -- news media organizations, social networking sites, online shopping companies, universities, and government agencies -- rent compute time from the cloud provider during which they can run their entire software stack on the cloud provider's server. The cloud providers are able to provide cheap computing power by letting multiple client operating systems share a single physical machine, and they use virtualization technology to do that. The virtualization layer also provides isolation between guests, protecting each from unwanted access by the co-tenants.

In this talk I will discuss my research toward verifying the security of this virtualization layer, and in particular, the isolation properties. I will discuss some of the challenges and opportunities in using traditional formal methods to verify security properties at this level of the software stack, and I will present a new methodology, based on model checking, for handling one of the biggest challenges: verification in the face of very large data structures. One weakness of using model checking is that the verification result is only as good as the model; I will also present work I've done to give stronger confidence in the validity of the model.