EPSRC logo

Details of Grant 

EPSRC Reference: EP/K032089/1
Title: Certified Verification of Client-Side Web Programs
Principal Investigator: Gardner, Professor P
Other Investigators:
Maffeis, Dr S
Researcher Co-Investigators:
Project Partners:
Google INRIA Mozilla Foundation
University of Leuven
Department: Dept of Computing
Organisation: Imperial College London
Scheme: Standard Research
Starts: 30 September 2013 Ends: 28 February 2017 Value (£): 893,923
EPSRC Research Topic Classifications:
Fundamentals of Computing Software Engineering
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
23 Jan 2013 EPSRC Research Institute APA & V Announced
Summary on Grant Application Form
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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.imperial.ac.uk