Speaker Jason Franklin
Host Helen Wang
Affiliation MSR Intern
Date recorded 27 August 2010
We describe our in-progress efforts to verify safety and liveness properties of a kernelized web browser model (with as little effort as possible). Kernelized web browsers partition the traditional monolithic browser architecture into two parts: 1) a browser kernel that includes security-relevant functionality and 2) a less privileged user-level component. The browser kernel's goal is to constrain malicious users from violating the integrity or confidentiality of honest users.
The focus of this talk will be on our security-centric verification methodology including:
We discuss insights gleaned from the verification process including how secure systems can be designed to reduce verification costs, some potential future directions that promise to further reduce verification costs, and open questions that we’d love help answering. No background in verification or browsers is necessary to understand this talk.
©2010 Microsoft Corporation. All rights reserved.