EPSRC logo

Details of Grant 

EPSRC Reference: EP/N019547/1
Title: Verification of Web-based Systems (VOWS)
Principal Investigator: Popescu, Dr A A
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Caritas Anchor House Max Planck Institutes Technical University of Munich
Department: Faculty of Science & Technology
Organisation: Middlesex University
Scheme: First Grant - Revised 2009
Starts: 01 April 2016 Ends: 31 March 2018 Value (£): 100,933
EPSRC Research Topic Classifications:
Fundamentals of Computing Information & Knowledge Mgmt
Software Engineering
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
20 Oct 2015 EPSRC ICT Prioritisation Panel - Oct 2015 Announced
Summary on Grant Application Form
In this project, we are concerned with the verification of information-flow security of web applications, more precisely, with confidentiality properties: users of a web-based system should not be able to *infer*, let alone access, some designated sensitive information.

For example, consider a system that stores information about medical patients and offers selective web-based access to individuals and companies. A life insurance company agent should not be given direct access to sensitive information such as a registered patient suffering from cancer. However, ideally the system should also prevent propagation of sensitive information: if it is known that certain discounts are offered mainly to patients suffering from cancer, then the agent can infer that sensitive information if they can access the list of available discounts for that patient.

A proof assistant is an environment for building mathematical models of reality, in particular, of software systems, and mechanically verifying properties about them. A web framework is an environment for writing web applications. The behaviour of a web application can be regarded as an input/output (I/O) automaton: a user interacts with the web application by submitting input (e.g., through the fields of the web forms); in response, the application changes its internal state and outputs a new web page. The I/O automaton model captures the essential information flow through a web application.

We build an infrastructure for verifying the information flow of web applications in a proof assistant. To this end, we design and implement a tool for the automatic translation of web applications written in a web framework into mathematical models in a proof assistant, namely I/O automata. Moreover, in the proof assistant, we formalize a framework for the verification of information-flow security for I/O automata, addressing aspects such as proof automation and compositionality. To validate this entire mechanism, translation plus verification of web applications, we perform a major case study: a confidentiality-verified social media platform.
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
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
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.mdx.ac.uk