Grants and Fellowships


Automated Generation and Detection of Exploits via Incorrectness Logic

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

Summary

Coming soon!


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 (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) (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]

Awards

  • 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