TWC: Medium: Towards a Formally Verified Web Browser

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

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.