Certified Verification of Client-Side Web Programs

点击翻译按钮获取中文摘要

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.