Security verification

Security verification – obtaining mathematical proof of the behaviour of systems and pieces of hardware – is embedded into many of our projects, ensuring that formal guarantees are built into emerging technologies.

Overview

Our researchers are experts in correctness, liveness (ensuring that the technology is always ready to take the next step) and verification of security properties (ensuring that the system is not behaving in an insecure way).

Projects

5G Tech-Sec

The advent of 5G – the next generation of mobile communications which will underpin technologies such as autonomous vehicles and smart cities – brings new challenges in terms of security verification.

In a joint project between us and Surrey’s 5G/6G Innovation Centre (5G/6GIC) – 5G Tech-Sec – researchers will develop new formal models, verification mechanisms and tools for the analysis of security and privacy of 5G systems against 5G-specific security and privacy risks such as threats stemming from reconfigurable networks and the arbitrary number of connections to a 5G small-cell.

  • Budget: £115,000
  • Funding body: NCSC
  • Centre Lead: Dr Ioana Boureanu
  • Co-Investigator: Dr Zhili Sun (5G/6GIC)
  • Partners: BT
  • Timeframe: October 2019 - January 2023.

AutoPaSS (Automatic Verification of Complex Privacy Requirements in Unbounded-Size Secure Systems)

Today’s devices execute tasks concurrently in numerous and hyper-connected ways, so we need reliable system-analysis techniques which capture not only cybersecurity properties but also modern connectivity. Importantly, this becomes an even bigger challenge if we need to robustly analyse rich and complex properties such as anonymity and users’ untraceability.

The aim of the AutoPaSS project is to address this gap in the formal verification of secure systems. In the project, a team led by Dr Ioana Boureanu will develop formal methods and software-tools needed to analyse security and, especially, privacy in modern communications systems. 

  • Budget: £300,000
  • Funding body: EPSRC
  • Centre lead: Dr Ioana Boureanu
  • Partners: Vector GB Ltd, Thales
  • Timeframe: July 2019 - June 2022.

Verifiably correct transactional memory

Multi-core computing architectures have become ubiquitous over the last decade. To ensure correctness, concurrent programs on multicore systems must be properly synchronised, but synchronisation invariably introduces sequential bottlenecks, causing performance to suffer.

This project addresses programmability of concurrent programs through the use of transactional memory, focusing on some of the main challenges surrounding this, and taking the key steps necessary to facilitate wide-scale adoption.

In particular, the team will develop theoretical advances in our understanding of transactional memory correctness, methodological advances in verification techniques for it, and pragmatic advances via the development of application-aware transactional memory designs. Verification tools will support each of these steps.

  • Budget: £397,680
  • Funding body: EPSRC
  • Centre lead: Dr Brijesh Dongol
  • Partners: University of Sheffield, University of Kent associate partners: ARM Ltd, Mozilla Limited, De Paul University, University of Augsburg, University of Paderborn, University of Queensland, Victoria University of Wellington
  • Timeframe: 2018 - 2021.