| EPSRC Reference: |
EP/V000470/1 |
| Title: |
CapC: Capability C semantics, tools and reasoning |
| Principal Investigator: |
Batty, Dr M |
| Other Investigators: |
|
| 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 Date | Panel Name | Outcome |
|
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
|
|
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 |