| EPSRC Reference: |
EP/K032089/1 |
| Title: |
Certified Verification of Client-Side Web Programs |
| Principal Investigator: |
Gardner, Professor P |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
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: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
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 |