Supervisor

Suitable for

Abstract

Prerequisites:  Some knowledge of programming language semantics or verification, functional programming

 

I am happy to supervise MSc and Part C projects around verification and testing of systems software. Students should ideally have some knowledge of programming language semantics or verification; functional programming experience is useful.

Background

Systems software – operating systems, hypervisor, firmware, etc. – is notoriously difficult to reason about formally, due to the complex invariants and programming idioms it relies on, and due to its interaction with the underlying hardware. Recent advances in software verification include verified OS kernels and hypervisors, but practical verification of real-world systems above realistic semantics remains an open problem. The goal of the CN type system [2] is to enable practical verification of systems software written in C. CN builds on the Cerberus C semantics [3] and combines refinement types and separation logic [1] to reason about C code based on a notion of memory ownership.

Focus

There are several directions for possible related projects. In the following I give two examples as a starting point for discussions, but interested students are welcome to contact and meet me to discuss options.

• Separation Logic Testing. Recent work in this area [4] includes executable testing against separation logic specifications: even when proof is the goal, runtime testing against CN specifications lets one discover specification or code errors early, before embarking on proof, and quickly gain more confidence in both. The existing Fulminate tooling makes specifications executable by translating them into C assertions and instrumenting the target code.

This project explores an alternative: extending the Cerberus model to support testing C code against CN specifications directly within the Cerberus interpreter, to make testing sound with respect to C's complex semantics, and to simultaneously catch undefined behaviour and specification violations. Possible extensions include (a) using the interpreter-based implementation to explore extensions to CN's specification language (making use of the greater flexibility compared to compilation to C), or (b) exploiting the extended Cerberus for debugging proof failures, by replaying and explaining verification counterexamples in the interpreter.

• CN in Lean. CN automates large parts of the proof by sending proof obligations to an SMT solver. To ensure reliable automatino, the solver is only given problems in a decidable fragment of first-order logic, allowing users to fall back to manual proof where this is insufficient: user-specified lemmas can be exported and manually verified in an interactive theorem prover. This project explores whether verification can be made more practical by re-creating a CN-like system – possibly significantly cut-down – inside the interactive theorem prover Lean, to provide a smoother integration of SMT automation with manual proof.

 

References

[1] Separation Logic: A Logic for Shared Mutable Data Structures. John C Reynolds, 2002. https://www.cs.cmu.edu/~jcr/seplogic.pdf

[2] CN: Verifying Systems C Code with Separation-Logic Refinement Types. Christopher Pulte, Dhruv C Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami, 2023. https://www.cs.ox.ac.uk/people/christopher.pulte/popl23.pdf

[3] Into the Depths of C: Elaborating the De Facto Standards. Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert NM Watson, Peter Sewell, 2016. https://www.cl.cam.ac.uk/~km569/into_the_depths_of_C.pdf

[4] Fulminate: Testing CN Separation-Logic Specifications in C. Rini Banerjee, Kayvan Memarian, Dhruv Makwana, Christopher Pulte, Neel Krishnaswami, and Peter Sewell, 2025. https://www.cs.ox.ac.uk/people/christopher.pulte/2024-cn-testing-paper.pdf