The Web is evolving at enormous speed from a collection of mainly static web pages to the current huge dynamic ecosystem where the boundary between web pages and software application has become indistinct (e.g. Google maps). This effect is so pronounced that industry is beginning to view the Web as an operating system: e.g., Google’s Chrome OS and Firefox OS. This quick transformation has come at a price. We are stuck with dynamic languages developed for the early Web. These languages are unsuited to the development of sophisticated web applications, resulting in modern applications being either overly conservative or needlessly unreliable and insecure. JavaScript is the most widely used language for client-side web programming: that is, in the web browser. Initially, JavaScript was well-suited for the small web-programming tasks being asked of it. With the modern Web however, the demands placed on JavaScript have been huge. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy, untrusted code.
This project will provide a certifying verification tool for JavaScript to assert that e.g. a particular web application will maintain the structure of a web page and not leak security information, or that a browser extension will only perform permitted file system operations. Our tool will automatically generate proofs which will be certified (checked) by the well-known Coq proof assistant. Our ambitious aim is to ensure that the software we use to communicate with our banks is at least as reliable as the software as our banks use to communicate with each other.
