EPSRC logo

Details of Grant 

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:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
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
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.st-and.ac.uk