| EPSRC Reference: |
EP/N024222/1 |
| Title: |
Type-driven Verification of Communicating Systems |
| Principal Investigator: |
Brady, Dr EC |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of St Andrews |
| Scheme: |
First Grant - Revised 2009 |
| Starts: |
01 May 2016 |
Ends: |
30 April 2017 |
Value (£): |
93,995
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
02 Dec 2015
|
EPSRC ICT Prioritisation Panel - Dec 2015
|
Announced
|
|
|
Summary on Grant Application Form |
It is considered a fact of life that computer software routinely fails. Often, this is merely inconvenient. When a PC, tablet or mobile phone crashes, we can restart it, perhaps losing only a small amount of work. On the other hand, errors in systems software or in network or security infrastructure can be disastrous. Recent high profile security vulnerabilities such as the "Heartbleed" bug show that even well tested and widely used software can contain serious and undetected flaws.
This project forms the initial part of an ambitious long term vision of a platform for full-stack verified software development, accessible by
both programming practitioners and researchers. We will use a type-driven approach to software verification, using the dependently typed programming language Idris.
The promise of dependently typed languages is that we can, in principle, guarantee important functional properties of software (such as preservation of size and ordering properties of data) and extra-functional properties such as resource safety (for example, that a protocol is followed accurately). However, proving such properties in general remains impractical for typical application developers, due to the difficulty of constructing proofs, the difficulty of reading and maintaining software due to proof details interfering with the details of an algorithm, and the lack of robustness and efficiency in even state of the art implementations of dependently typed languages.
Idris aims to address these problems, having been built specifically with the goal of generating good quality executable code which can interroperate with existing systems. Furthermore, it supports language constructs for building "Domain Specific Languages" (DSLs). In this project, we will further develop Idris, focussing on robustness and efficiency, and show how its support for DSL construction and type-level programming allow us to develop secure communication protocol implementations, described as a type-level DSL and verified by type checking.
In particular, we will construct verified implementations of Diffie-Hellman key exchange, and the Needham-Schroeder-Lowe protocol, and use these to implement a demonstrator application. This application (a networked chat system) will support secure communication (up to the guarantees given in the protocols), be efficient (no overhead due to proof obligations) and be able to communicate with alternative implementations in other languages.
|
|
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.st-and.ac.uk |