Awards

  • Distinguished Paper Award, Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2022
  • Distinguished Artifact Award, European Symposium on Programming (ESOP), 2022
  • Imperial College President’s Award for Excellence in Research (Early Career Researcher), 2021
  • Best Paper Award, IEEE Conference on Games (CoG), 2019

Grants and Fellowships


SACRED-MA: Safe and Secure Remote Direct Memory Access

EPSRC Standard Grant
Duration: September 2023 August 2026
Joint Principal Investigator
Amount: £750,000

Summary

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.


UK Research Institute on Verified Trustworthy Software Systems

Directorship of the UK Research Institute Verified Trustworthy Software Systems (VeTSS)
Duration: December 2022 November 2026
Co-Director
Amount: £750,000

Summary

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).


Automated Generation and Detection of Exploits via Incorrectness Logic

Meta research gift through the Privacy Aware Program Analysis Request for Proposals scheme
Duration: November 2022 October 2023
Sole Investigator
Amount: $50,000

Summary

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.


Related Publications

  • Concurrent Incorrectness Separation Logic
    Azalea Raad, Josh Berdine, Derek Dreyer, Peter O'Hearn
    Principles of Programming Languages (POPL), 2022
    [Paper] [@ACM]

  • Local Reasoning about the Presence of Bugs: Incorrectness Separation Logic
    Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn
    Computer-Aided Verification (CAV), 2020
    [Paper] [@Springer]

PERSEVERE: A Rigorous Foundation for Persistent Verification

UKRI Future Leader fellowship
Duration: October 2021 September 2025
Sole Investigator
Amount: £1,500,000

Summary

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:

  • develop formal, comprehensive persistency models for mainstream hardware architectures;
  • define formal persistency models for mainstream programming languages; and
  • devise effective testing and verification techniques for persistent programming.


Project Publications

  • Finding Real Bugs in Big Programs with Incorrectness Logic
    Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, Peter O'Hearn
    Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2022
    [Paper] [@ACM] [Artifacts available] [Artifacts evaluated & reusable]

  • View-Based Owicki-Gries Reasoning for Persistent x86-TSO
    Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson
    European Symposium on Programming (ESOP), 2022
    Winner of the Distinguished Artifact Award!
    [Paper] [@Springer] [Artifacts available] [Artifacts evaluated & reusable]

  • Extending Intel-x86 Consistency and Persistency
    Azalea Raad, Luc Maranget, Viktor Vafeiadis
    Principles of Programming Languages (POPL), 2022
    [Paper] [@ACM] [Artifacts available] [Artifacts evaluated & reusable]

  • Concurrent Incorrectness Separation Logic
    Azalea Raad, Josh Berdine, Derek Dreyer, Peter O'Hearn
    Principles of Programming Languages (POPL), 2022
    [Paper] [@ACM]

Related Publications

  • Revamping Hardware Persistency Models
    Kyeongmin Cho, Sung-Hwan Lee, Azalea Raad, Jeehoon Kang
    Programming Language Design and Implementation (PLDI), 2021
    [Paper] [@ACM] [Artifacts available] [Artifacts evaluated & reusable]

  • PerSeVerE: Persistency Semantics for Verification under Ext4
    Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, Viktor Vafeiadis
    Principles of Programming Languages (POPL), 2021
    [Paper] [@ACM] [Artifacts available] [Artifacts evaluated & reusable] [Artifacts functional & reusable]

  • Persistent Owicki-Gries Reasoning
    Azalea Raad, Ori Lahav, Viktor Vafeiadis
    Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2020
    [Paper] [@ACM]

  • Persistency Semantics of the Intel-x86 Architecture
    Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeadis
    Principles of Programming Languages (POPL), 2020
    [Paper] [@ACM]

  • Weak Persistency Semantics from the Ground Up
    Azalea Raad, John Wickerson, Viktor Vafeiadis
    Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2019
    [Paper] [@ACM]

  • Persistence Semantics for Weak Memory
    Azalea Raad, Viktor Vafeiadis
    Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2018
    [Paper] [@ACM]

Validating the Foundations of Verified Persistent Programming

UKRI VeTSS (UK Research Institute in Verified Trustworthy Software Systems)
Duration: April 2020 March 2021
Principal Investigator
Amount: £100,000

Summary

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.


Related Publications

  • View-Based Owicki-Gries Reasoning for Persistent x86-TSO
    Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, John Wickerson
    European Symposium on Programming (ESOP), 2022
    Winner of the Distinguished Artifact Award!
    [Paper] [@Springer] [Artifacts available] [Artifacts evaluated & reusable]

  • Extending Intel-x86 Consistency and Persistency
    Azalea Raad, Luc Maranget, Viktor Vafeiadis
    Principles of Programming Languages (POPL), 2022
    [Paper] [@ACM] [Artifacts available] [Artifacts evaluated & reusable]

  • Revamping Hardware Persistency Models
    Kyeongmin Cho, Sung-Hwan Lee, Azalea Raad, Jeehoon Kang
    Programming Language Design and Implementation (PLDI), 2021
    [Paper] [@ACM] [Artifacts available] [Artifacts evaluated & reusable]

  • PerSeVerE: Persistency Semantics for Verification under Ext4
    Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, Viktor Vafeiadis
    Principles of Programming Languages (POPL), 2021
    [Paper] [@ACM] [Artifacts available] [Artifacts evaluated & reusable] [Artifacts functional & reusable]

  • Persistent Owicki-Gries Reasoning
    Azalea Raad, Ori Lahav, Viktor Vafeiadis
    Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2020
    [Paper] [@ACM]

  • Persistency Semantics of the Intel-x86 Architecture
    Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeadis
    Principles of Programming Languages (POPL), 2020
    [Paper] [@ACM]

  • Weak Persistency Semantics from the Ground Up
    Azalea Raad, John Wickerson, Viktor Vafeiadis
    Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2019
    [Paper] [@ACM]

  • Persistence Semantics for Weak Memory
    Azalea Raad, Viktor Vafeiadis
    Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2018
    [Paper] [@ACM]