Certified Verification of Client-Side Web Programs

Web正以极快的速度从一个主要由静态网页组成的集合发展成为目前巨大的动态生态系统，在这个生态系统中，网页和软件应用之间的界限已经变得模糊（例如谷歌地图）。这种影响是如此明显，以至于业界开始将网络视为一个操作系统：例如b谷歌的Chrome OS和Firefox OS。这种快速转变是有代价的。我们受困于为早期Web开发的动态语言。这些语言不适合开发复杂的web应用程序，导致现代应用程序要么过于保守，要么不必要地不可靠和不安全。JavaScript是客户端web编程中使用最广泛的语言：也就是说，在web浏览器中。最初，JavaScript非常适合用于小型web编程任务。然而，随着现代网络的发展，对JavaScript的需求越来越大。JavaScript的动态特性使得理解它的代码非常困难，从而导致了错误和不可信的代码。这个项目将为JavaScript提供一个认证验证工具，例如，一个特定的web应用程序将维护一个网页的结构，而不是泄露安全信息，或者浏览器扩展将只执行允许的文件系统操作。我们的工具将自动生成证明，这些证明将由著名的Coq证明助手认证（检查）。我们雄心勃勃的目标是确保我们用于与银行沟通的软件至少与我们的银行用于彼此沟通的软件一样可靠。

The Web is evolving at enormous speed from a collection of mainlystatic web pages to the current huge dynamic ecosystem where theboundary between web pages and software application has becomeindistinct (e.g. Google maps). This effect is so pronounced thatindustry is beginning to view the Web as an operating system: e.g.,Google's Chrome OS and Firefox OS. This quick transformation has comeat a price. We are stuck with dynamic languages developed for theearly Web. These languages are unsuited to the development ofsophisticated web applications, resulting in modern applications beingeither overly conservative or needlessly unreliable and insecure.JavaScript is the most widely used language for client-side webprogramming: that is, in the web browser. Initially, JavaScript waswell-suited for the small web-programming tasks being asked ofit. With the modern Web however, the demands placed on JavaScript havebeen huge. The dynamic nature of JavaScript makes understanding itscode notoriously difficult, leading to buggy, untrusted code. Thisproject will provide a certifying verification tool for JavaScript toassert that e.g. a particular web application will maintain thestructure of a web page and not leak security information, or that abrowser extension will only perform permitted file systemoperations. Our tool will automatically generate proofs which will becertified (checked) by the well-known Coq proof assistant. Ourambitious aim is to ensure that the software we use to communicatewith our banks is at least as reliable as the software as our banksuse to communicate with each other.