Verifying Safety and Liveness Properties of a Kernelized Web Browser

Date

August 27, 2010

Speaker

Jason Franklin

Affiliation

MSR Intern

Overview

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:

  1. Specifying security properties including a novel formulation of noninterference,
  2. Fine-grained partitioning of security-relevant and irrelevant system components,
  3. Identifying the “right” level of abstraction to locate design flaws without getting bogged down in implementation issues, and
  4. Specifying realistic adversaries in a simple and intuitive way that avoids over-constraining their capabilities.

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.

Speakers

Jason Franklin

Jason Franklin is Ph.D. student at CMU under the advisement of Anupam Datta. He expects to graduate in 2011. He is the recipient of the NSF Graduate Research Fellowship, the 2009 SOSP best paper award for work on energy-efficient cluster systems for data-intensive computing (FAWN), and the 2005 Usenix Security best paper award for jointly discovering systemic vulnerabilities in Internet monitoring systems. His work has been featured in articles by major news organizations including CNBC and Newsweek along with trade press including CNET, Computer World, Information Week, MIT Technology Review, Slashdot, Slate, and ZDnet. These days he works on the theory of secure systems (a.k.a. science of security) with the goal of developing principled techniques to construct and reason about operating systems, web browsers, hypervisors, and other secure systems.

People