Certified Verification of Client-Side Web Programs

Web正在以巨大的速度从主要静态网页的集合发展到当前巨大的动态生态系统，其中网页和软件应用程序之间的边界变得模糊（例如Google地图）。这种影响是如此明显，以至于工业界开始将Web视为一种操作系统：例如，谷歌的Chrome操作系统和火狐操作系统。这种快速的转变是有代价的。我们被困在为早期网络开发的动态语言中。这些语言不适合开发复杂的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.