Summary

The main objective of this research is to seed a fundamental direction for program analysis tools, based on the recent theory of incorrectness logic (IL). Our aim is to develop a stable prototype that enables sound bug detection throughout the full life cycle of program development, from development in an IDE all the way to deployment to production. The two core principles of this prototype are accuracy (soundness) of bugs detected and ease of use for developers. This stable prototype will prime expanded scientific research, it will facilitate industrial development and collaboration, and most notably will lead to a future with sound bug detection for all, regardless of the size, budget or the experience levels of development teams.

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.

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

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]

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]


• 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]


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


• 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]


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


• 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]

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]


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


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


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


• 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]