School of Computing academics awarded Digital Security project grant from UKRI

A project from Dr Mark Batty and Dr Stephen Kell of Kent’s School of Computing has been named one of nine winners of the UKRI (UK Research and Innovation)’s Digital Security by Design £10m grant. Their project is part of the Digital Security by Design programme (DSbD), which takes a ground-up approach to improving UK resilience to cyber attacks.

DSbD is part of a UK Industrial Strategy Challenge Fund investment comprising a £70M government investment and a £117M industrial investment. DSbD will develop groundbreaking cyber security technologies, with the potential to prevent hackers from remotely taking control of digital systems such as smart home security systems as well as cyber attacks and data breaches, meaning people and online businesses are better protected. The Government will provide £10 million for academic work towards these aims over four years to the grant winners.

‘CapC: Capability C semantics, tools and reasoning’, is the winning project led by Dr Batty. The C language underpins nearly all of our computer systems. Dr Batty and his team have developed rigorous mathematical techniques to study the definition of the C language, discovering major problems in the language, and suggesting fixes. The Digital Security by Design programme will build a secure software stack, with Dr Batty’s semantic definition of C underpinning it.

Dr Batty said: ‘I am delighted to have been awarded this grant. It often surprises people to hear that the C language, central to nearly all computer systems, has flaws in its definition. We develop techniques to understand and improve the language definition, so that it can act as a solid basis for programmers and software verification. We have an excellent team here at Kent: co-investigator Stephen Kell is an expert on C’s toolchain infrastructure and its sequential semantics, researcher Simon Cooksey is an expert toolbuilder specialising in evaluating the C semantics, and I have expertise in the concurrency definition of C.

‘Our work should fit well in the DSbD project, underpinning the verification of security properties throughout the software stack. I hope DSbD can demonstrate the practical value of our research and that radically more secure systems are within reach.’