| 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: |
|
| 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: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
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
|
|
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.mdx.ac.uk |