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.