TWC: Medium: Towards a Formally Verified Web Browser

网络浏览器无处不在，不可或缺。它运行社交网络、商业生产力和网上银行等应用程序，并承诺隔离策略，以保证这些应用程序并排运行时的安全。因为它的关键作用，我们希望浏览器是强大的和安全的攻击；但实际上浏览器是脆弱的。它们是复杂的软件，具有丰富的功能，允许灵活性和可编程性，即使是小错误也会使浏览器容易受到攻击。事实上，浏览器漏洞已经被用来渗透美国国防承包商和领先科技公司的内部网络。提高浏览器安全性的尝试通常是特别的工程努力；即使提供了正式的保证，它们也以对浏览器模型或理想化的证明的形式出现，而不是浏览器本身。错误的实现可能会使预期的保证失效，并使用户容易受到攻击。这个项目的目标是在Coq校对助手中构建一个浏览器，并证明其正确性。与之前的研究成果不同，这次的证明涵盖了实际的浏览器实现，而不是一个模型或抽象。这为浏览器的安全属性提供了极其强大、精确的保证。通过将验证工作集中在一个小浏览器内核上，并在沙箱中运行遗留代码来渲染网页，证明变得容易处理。通过这种方式，浏览器可以提供有意义的隔离保证，即使在呈现网页的遗留代码不受信任且可能存在错误的情况下。该项目将提供：*为网络用户提供更可靠和安全的浏览器；*为软件开发人员提供开发高保证系统的新方法；*对于研究人员来说，一个关于安全策略的正式推理框架；*对于学生，安全与正规方法教育。

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.