EPSRC Standard Grant
Duration: September 2023 – August 2026
Joint Principal Investigator
The principle aim of SACRED-MA is to develop a formally verified RDMA stack, building up from formal hardware models to safe and secure distributed applications. We enable a correct-by-construction methodology that places safety and security at its heart. All our proofs will be mechanised using advances model checking and theorem proving tools to ensure a high level of rigour in our work, and eliminate the possibility of human error.
To this end, we propose a research plan centred around three objectives: 1) developing a rigorous foundation for RDMA at the lowest levels of abstraction, namely hardware and languages; 2) enabling RDMA programmability via reusable libraries for distributed systems; and 3) addressing RDMA trustworthiness via mechanised, formal proofs of correctness.
Directorship of the UK Research Institute Verified Trustworthy Software Systems (VeTSS)
Duration: December 2022 – November 2026
The Research Institute on Verified Trustworthy Software Systems (VeTSS) is a UK Academic Research Institute in Cyber Security. VeTSS is jointly hosted by the University of Surrey and Imperial College London, with Dr Azalea Raad (Imperial) and Dr Brijesh Dongol (Surrey) as co-directors.
One of four research institutes within the National Cyber Security Centre (NCSC), VeTSS brings together leading academics, industry professionals, regulators and government representatives to ensure research into software stays focused on the safety and security challenges faced by the UK and mitigates the risks posed. VeTSS succeeds the EPSRC funded VeTSS Research Institute hosted at Imperial College London and the previous Research Institute in Automated Program Analysis and Verification (RIAPAV).
Meta research gift through the Privacy Aware Program Analysis Request for Proposals scheme
Duration: November 2022 – October 2023
A crucial problem in large codebases with a high rate of bugs is how to determine which of these bugs have security implications, namely whether they can be exploited. Understanding the exploitability of bugs is a time-consuming manual process requiring expert knowledge. As a result, automated exploit generation and detection have become important areas of interest for researchers and software engineers. However, existing exploit analysis techniques have several limitations. Specifically, exploit generation techniques are often not scalable (as they do not support compositional reasoning) and not modular (they require a new approach to be devised from scratch for each new category of exploits), while exploit detection techniques often suffer from false positives (identifying innocuous code as exploits).
I propose a new approach to automating the generation and detection of software exploits underpinned by my work on concurrent adversarial separation logic (CASL), an extension of incorrectness logic (an under-approximate reasoning framework by O’Hearn) for exploits. Specifically, CASL is inherently under-approximate (guarantees the absence of false-positives), and enables compositional reasoning (allowing for local and efficient reasoning about exploits) and parametric definitions (allowing for the rapid adaptation of existing techniques to new exploits). I will develop a new technique for automatically generating software exploits along with a tool implementing it, as well as a cutting-edge automated exploit detection tool built on Meta’s Infer platform. This work will represent a major leap forward in the automation of software exploit generation and detection, and create practical tools for industry applications.
UKRI Future Leader fellowship
Duration: October 2021 – September 2025
Modern society depends on accessing and storing vast quantities of data, at ever-increasing speeds. To meet our conflicting desiderata of fast and durable (persistent) data, the cutting-edge non-volatile memory (NVM) technology provides fast, byte-addressable access at a performance comparable to DRAM, while ensuring persistence across crashes as with hard disks. NVM is expected to lead to substantial changes in how we manage storage in software, the huge performance gains of NVM are difficult to exploit correctly (without programming bugs).
The objective of my fellowship, PERSEVERE, is to develop the scientific and engineering underpinnings necessary for safe and ubiquitous NVM adoption in modern computing through rigorous, mathematical foundations. Specifically, as part of this fellowship I will:
UKRI VeTSS (UK Research Institute in Verified Trustworthy Software Systems)
Duration: April 2020 – March 2021
Non-volatile memory (NVM) is fast becoming mainstream, and with it comes the need to write programs that exploit it correctly and efficiently. To verify the correctness of such programs, we need formal models of how CPUs interact with NVM, answering questions such as: which stores are guaranteed to persist across crashes? And in what order do they persist? Previous work by the PIs has devised putative models; this project seeks to validate those models empirically against main- stream architectures such as Armv8 and Intel-x86. Key challenges include generating test cases that are capable of revealing the persistency behaviour of CPUs, and detecting which stores become per- sistent without continually power-cycling the CPU.