Verifying Safety and Liveness Properties of a Kernelized Web Browser

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.