EPSRC logo

Details of Grant 

EPSRC Reference: EP/T013516/1
Title: Verifying Resource-like Data Use in Programs via Types
Principal Investigator: Orchard, Dr DA
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Augusta University Galois, Inc
Department: Sch of Computing
Organisation: University of Kent
Scheme: New Investigator Award
Starts: 01 March 2020 Ends: 28 February 2022 Value (£): 229,328
EPSRC Research Topic Classifications:
Software Engineering
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
15 Jan 2020 EPSRC ICT Prioritisation Panel January 2020 Announced
Summary on Grant Application Form
Software is integral to the fabric of our lives, controlling transport, the economy and

infrastructure, and providing the main tools of work and leisure. The cost of software failures is

therefore high, to productivity, stability, safety, and privacy. As an indication of the economic

impact, it is estimated that software errors cost the US economy tens of billions of dollars last

decade. Software errors can also impact human safety as software is used to control transport,

infrastructure, and medical equipment. The research agenda of program verification aims to mitigate

these risks by putting software engineering on a rigorous foundation through techniques to guarantee

program correctness. As software becomes more complex and pervasive, program verification is ever

more important. This work aims to advance the state-of-the-art in verification at the point of

program development through advancements in programming language theory and practice.

Programming languages are the core tool in which software is constructed; they are the means of

communicating our intentions to computer hardware. There are various design trade-offs when creating

a programming language, which has led to the variety of programming languages in use today. Some

languages support verification by including a "type system" which categorises data and operations,

ensuring that operations are only applied to data of the correct type. This provides some guarantees

about the correctness of the program by ruling out various kinds of error before the program is ever

executed. A subfield of programming language research aims to make type systems more expressive so

that they can describe and enforce more properties of programs and thus raise the level of

verification possible within the language. The current proposal aims to do just this, focussing on

the notion of data as a "resource" subject to constraints which should be enforced by a language's

type system. This project develops a particular technique for building such type systems in a way

that can capture various kinds of property in one system.

The manipulation of data is central to the task of programming. Current programming languages

essentially view data as an infinitely-replicable resource that can be stored, manipulated, and

communicated without restriction. However, this perspective is naive. Some data is private and thus

should not be arbitrarily copied, stored, or communicated. Some data is large and thus should not be

replicated too frequently. Some data acts as a way of interfacing with other parts of a system,

e.g., files or communication channels, which are then subject to restrictions on how they can be

used, such as agreed protocols of interaction. Most programming languages are agnostic to these

constraints however, treating data as totally unconstrained. This can lead to various software

errors, including privacy breaches, performance problems, and crashes due to incorrect interactions

between parts of a system. The goal of this research is to embed the constraints associated with

data into the type system of a language so that these additional constraints can be automatically

enforced. The key technology for doing this is a novel notion of types called "graded modal types"

which can capture and track different kinds of information about the structure of programs and the

flow of data through them.

This work will develop the theory and practice of graded modal types, producing a prototype language

that demonstrates their use for verifying program properties. Three case studies will be carried out

to demonstrate their power: (1) ensuring privacy and confidentiality, (2) capturing and reasoning

about performance e.g., how fast a program will execute relative to the size of its inputs and how

much memory it will consume (3) enforcing fine-grained protocols of interaction.

This work is a step towards a new generation of trustworthy software.
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.kent.ac.uk