Certified Verification of Client-Side Web Programs

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.

A study by Boston Consulting Group 4 found that 8% of the UK GDP is
generated through the Internet. This share is expected to grow to 12%
by 2016, projecting the UK economy to become the world's most
internet-dependent economy. Meanwhile, the Cybersecurity position
statement of Research Council UK quotes the cost of cybercrime to the
UK in 2010 at £27 billion. This will inevitably rise as the UK becomes
more dependent on the Internet. The Web can only function as an
instrument of wealth creation if the programs that are used to access
it are robust, reliable and secure.

We will produce a variety of certifying verification tools, supported
by Coq and with a strong empirical link to industrial languages.
These verification tools will provide much needed support for the
engineers that build the Web.

Tasks 1-2. We provide systematic comparisons between browser
implementations and ECMA reference implementations. Library authors
will be interested in the comparisons between browser implementations,
because they will want their libraries to work on all
browsers. JavaScript implementers will be interested in the ECMA
reference implementations.

Task 3. We will provide the principled development of a core
certifying verification tool for JavaScript, rooted in the Coq
specifications given in Tasks 1-2. The main industrial impact will be
through Task 6.

Task 4. We will provide a library plugin interface for e.g. DOM, with
simple connections to the well-known academic and industrial
verification tools based on separation logic.

Task 5. Working with Miller from Google California, we will provide a
formal description of Secure ECMAScript (SES), proofs that
e.g. Google's makeContractHost enforces contracts between mutually
untrusting parties, and a proof that the SES implementation in
JavaScript is indeed secure.

Task 6. We will build specific, usable development tools for
JavaScript based on JSVerify and the DOM plugin, with the guidance of
Mozilla engineers. E.g., we will assist a web application developer to
produce bug-free apps and a security analyst to review Firefox addons.


This proposal is highly ambitious, ranging from a Coq specification of
a real-world language through to industrially-accepted certifying
development tools. However, our recent research and discussions with
key industrial engineers suggest that these aims are not beyond reach.