TWC: Medium: Towards a Formally Verified Web Browser

点击翻译按钮获取中文摘要

The web browser is ubiquitous and indispensable. It runs applicationslike social networking, business productivity, and online banking, andpromises isolation policies that keep these applications secure whenrun side-by-side. Because of its crucial role, we would like thebrowser to be robust and secure against attack; but in fact browsersare fragile. They are complex pieces of software with rich featuresthat allow for flexibility and programmability, and even small bugscan make the browser vulnerable to attack. Indeed, browservulnerabilities have been used to infiltrate the internal networks ofAmerican defense contractors and leading tech firms. Attempts toimprove browser security are often ad-hoc engineering efforts; andeven when formal guarantees are provided, they come in the form ofproofs over a model or idealization of the browser, not the browseritself. A buggy implementation can invalidate intended guarantees andleave users open to attack.The goal of this project is to build a browser inside the Coq proofassistant, along with a proof of its correctness. Unlike previousresearch efforts, the proof covers the actual browser implementationrather than a model or abstraction. This provides extremely strong,precise guarantees about the security properties of the browser. Theproof is made tractable by focusing the verification effort to a smallbrowser kernel, and running legacy code in a sandbox to renderweb pages. In this way, the browser can provide meaningful isolationguarantees even when the legacy code that renders web pages isuntrusted 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.