Secure Virtualization with Formal Methods
Speaker: Cynthia Sturton, University of California, Berkely
Series: Electrical Engineering Departmental Seminar
Location:
Engineering Quadrangle B205
Date/Time: Monday, April 8, 2013, 4:30 p.m.
- 6:00 p.m.
Abstract:
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.
Biography:
Cynthia Sturton is a Ph.D. candidate in Computer Science at the University of California, Berkeley. She received her B.S.E. in Computer Systems Engineering from Arizona State University, and her M.S. in Computer Science from UC Berkeley. Her research focuses on the verification of security-relevant properties in practical systems using formal methods. She is a member of the Intel Science and Technology Center for Secure Computing and is a recipient of the UC Berkeley Chancellor's Fellowship.
