| 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: |
|
| Department: |
Sch of Computing |
| Organisation: |
University of Kent |
| Scheme: |
New Investigator Award |
| Starts: |
01 July 2020 |
Ends: |
30 June 2023 |
Value (£): |
229,328
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
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 |