The web browser is ubiquitous and indispensable. It runs applications like social networking, business productivity, and online banking, and promises isolation policies that keep these applications secure when run side-by-side. Because of its crucial role, we would like the browser to be robust and secure against attack; but in fact browsers are fragile. They are complex pieces of software with rich features that allow for flexibility and programmability, and even small bugs can make the browser vulnerable to attack. Indeed, browser vulnerabilities have been used to infiltrate the internal networks of American defense contractors and leading tech firms. Attempts to improve browser security are often ad-hoc engineering efforts; and even when formal guarantees are provided, they come in the form of proofs over a model or idealization of the browser, not the browser itself. A buggy implementation can invalidate intended guarantees and leave users open to attack.
The goal of this project is to build a browser inside the Coq proof assistant, along with a proof of its correctness. Unlike previous research efforts, the proof covers the actual browser implementation rather than a model or abstraction. This provides extremely strong, precise guarantees about the security properties of the browser. The proof is made tractable by focusing the verification effort to a small browser kernel, and running legacy code in a sandbox to render web pages. In this way, the browser can provide meaningful isolation guarantees even when the legacy code that renders web pages is untrusted and potentially buggy.
This project will provide: * For users of the web, browsers that are more reliable and secure; * For software developers, a new approach for developing high-assurance systems; * For researchers, a framework for formally reasoning about security policies; * For students, security and formal methods education.
