DATE: Thursday, October 3, 2013
TIME: 12:00 - 1:00 pm
PLACE: GHC 8102
SPEAKER: Limin Jia, Carnegie Mellon University
TITLE: The Design, Implementation, and Verification of an Extensible Hypervisor Framework
ABSTRACT:
Formal verification of system properties is crucial to the security of software systems. Combing the design, implementation, and verification of software systems can significantly ease the process of verification, and produce high-assurance systems. In this talk, I will present our work on XMHF – an eXtensible and Modular Hypervisor Framework. XMHF's design aims to achieve modular extensibility and automated verification. The design enables us to verify the memory integrity property of XMHF by breaking the verification into two stable portions: (1) we identify local properties required of the source code, which are verified automatically using the C model checking tool CBMC; and (2) an inductive manual proof that uses these local properties as assumptions to show that the memory integrity property holds on XMHF even when interacting with malicious guest OSes. The verification of the source code can be repeated automatically in the development phase when the code is modified. The second part of verification is carried out using a novel program logic that we develop to reason about the trace properties of systems in the presence of adversaries.
BIO:
Limin Jia received her B.E. in Computer Science and Engineering from the University of Science and Technology of China and her Ph.D. in Computer Science from Princeton University. Her research interests include language-based security, programming languages, logic, and program verification. Limin's research focuses on formal aspects of security. She is particularly interested in applying language-based security techniques as well as formal logic to model and verify security properties of software systems.
SDI / ISTC SEMINAR QUESTIONS?
Karen Lindenfelser, 86716, or visit www.pdl.cmu.edu/SDI/