Verifying Resource-like Data Use in Programs via Types

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.

The pervasive nature of software in our society means that the tools used for creating software have
wide-reaching impact. Programming languages in particular impact the ability of software engineers
(developers) to read, write, and reason about their programs, as well as the ability of computers to
effectively execute programs. This project is primarily concerned with making it easier for
developers to reason about the use of data in their programs, and to ensure that extra-functional
constraints associated to data (e.g., confidentiality) are respected. This kind of reasoning is
particularly important for developers of software used in high-risk contexts, e.g., travel, medical
applications, infrastructure, and for developers of software that handles sensitive data, e.g.,
mobile phone apps, websites, financial services. The techniques to provide this enhanced ability
for program reasoning and verification involve scientific advances in the area of programming
language theory. The practical application of this theory will deliver a novel programming approach,
exemplified in a new language which can assist program verification. Thus this project will deliver
complementary impact across both academia and industry, and further to society and the economy via
its impact in the software development industry.

In terms of industrial impact, and beyond, there are two many routes in which the main practical
deliverable, the language Granule, can have impact: (1) by becoming a mature programming language
that can be used by developers; (2) by influencing the design of existing and future programming
languages. Within the lifetime of this project, the latter mode of impact is the most likely, though
the impact activities here support both routes to delivering impact.

The Granule implementation will be open source, allowing ideas to be easily adopted by other
language implementers and encouraging a community of developers to grow, contributing to Granule
directly. The language will be promoted online, including via a series of online tutorial videos,
written tutorials, and online documentation. In the second year of the project, an online hackathon
competition will be run to promote Granule and to encourage early contributions and feedback from
practitioners. Industry talks will also be given and an academic workshop at the end of year 1 will
also be open to industrials. All these impact activities will not only help to promote the work to
industry and other language implementors, but will also assist the academic impact as well.

The impact and popularity of a language often relates to the amount and quality of library
support. Therefore, there will be a focus in the second year of the project on improving the
libraries and encouraging development of these by others outside the project team (see above).

Running throughout the project are three key practical application case studies: privacy, cost, and
protocols. The case studies will help to ensure that the research links with practical
applications, and will then serve as a way to demonstrate the verification technique developed
here. The privacy case study is in collaboration with industrial partner Galois Inc., and is
particularly relevant in the context of modern software development, where privacy is increasingly a
concern and there are increasing legal requirements to meet data protection standards.

Following from the industrial impact, the benefits to society and the economy are then yielded in
terms of correct and trustworthy software, with fewer bugs, which in turn reduces the cost of
software and reduces risk to stability, safety, and privacy. Take together, the long-term goals of
the project help to support a more rigorous engineering foundation for the UK's considerable
software industry, and further afield.