EPSRC logo

Details of Grant 

EPSRC Reference: EP/V000470/1
Title: CapC: Capability C semantics, tools and reasoning
Principal Investigator: Batty, Professor M
Other Investigators:
Kell, Dr S R
Researcher Co-Investigators:
Project Partners:
Department: Sch of Computing
Organisation: University of Kent
Scheme: Standard Research
Starts: 01 August 2020 Ends: 31 July 2023 Value (£): 485,168
EPSRC Research Topic Classifications:
Fundamentals of Computing Software Engineering
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:
Panel DatePanel NameOutcome
06 Apr 2020 ISCF Digital Security by Design Research Projects Announced
Summary on Grant Application Form
We address a difficult technical problem that is drawn from industry:

we seek a solution to fundamental problems found in the standards of

the C and C++ programming languages. C and C++ code is not just

prevalent -- it is used to form the lowest and most trusted levels of

our systems. The kernel of every mainstream operating system uses some

combination of the two, including Windows, MacOS, iOS, Android, Linux

and Unix, as do the swathe of embedded controllers with essential

functions like automotive engine management. Having a good

specification of the language is the first step in verifying the

correctness of these vital system components.

-- Combatting software failure --

This work is part of a larger effort to combat software failure by

developing techniques to verify the correctness of software.

Currently, developers of computer systems rely predominantly on

testing to ensure that systems behave as they should. The system is

run for some time over various inputs and monitored for failure. The

hope is that this will expose enough of the flaws in the system to

make it reliable once it is deployed. But it is increasingly

expensive to achieve good coverage: systems like cars experience

wildly varied inputs, and a fleet of a particular model of car runs

collectively for far longer than the time its computer systems are

tested. Worse still, modern systems are concurrent -- using multiple

communicating processors to complete a task. The delicate interplay

between the concurrent processors makes the output of the system

dependent on the timing of communication, so that some behaviours

occur only a handful of times in billions of runs, leaving testing

little hope of finding associated bugs. When scrutinising security

properties, one is faced not with simple circumstance, but with a

committed adversary that cannot be replicated by simple testing.

There is evidence that validating software through testing is breaking

down and some bugs are evading discovery even in critical systems: for

example a concurrency bug caused some of Toyota's cars to suddenly and

relentlessly accelerate, killing 83 over 10 years. The wider economic

cost of software failure was estimated by the U.S. National Institute

of Standards and Technology to cost USD 60bn each year. Improving our

approach to software failure would have substantial economic and

societal impact.

Verification offers an alternative to testing: one defines desirable

properties of the system -- it will not crash, fuel metering will be

proportional to accelerator input, and so on -- and mathematically

proves that the code satisfies them. In the ideal of verification,

there is no space for bugs to creep in and the mathematical proof of

correctness is absolute. This is particularly valuable for security

properties. Unfortunately, verification techniques are invariably

built above an idealised model of the computer system, e.g.\ the

assumption that memory accesses take place in a global sequential

order, so called sequential consistency (SC). The distance between the

ideal and the reality leaves ample space for bugs to persist. In fact

the status quo is much worse because we do not have a characterisation

of the reality of the system's behaviour: our best models of

programming-language behaviour are known to be broken, e.g.\ in C, C++

and Java.

In this broad context, our project will develop a description the C

language that matches the reality, permitting the sorts of behaviour

exhibited by compiler optimisations and the underlying concurrent

processors. At the same time, we will develop verification techniques

in a setting that correctly models the subtle behaviour of modern

languages, dovetailing these previously disparate views of the

system. Our work will make verification of concurrent systems more

viable, including security properties, helping to address the economic

and social costs of software failure.
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.kent.ac.uk