LFCS Seminar: Tuesday 14th April: Rini Banerjee | LFCS

Tue, 14 Apr, 4.10pm

Venue: IF G.03

Remote participation:

URL: https://ed-ac-uk.zoom.us/j/89292150989

Password: HjWE0rem

Title: Gradual Assurance for Systems Software: A Separation-Logic Approach

Abstract

The conventional code-test-debug cycle is the de-facto methodology

for building software systems, and while successful to an extent, it

manifestly fails to make these systems reliable enough. Various

approaches have been explored over the past few decades to improve the

reliability of these systems, from push-button static and dynamic

analysis tools to traditional formal verification via rich, explicit

specifications. These specifications require specialist expertise

to write and are therefore costly to produce and maintain, especially

at scale. Testing specifications concretely at runtime — as they are

being written — can alleviate this by making it possible to check and

debug in-progress, partial specifications in a lightweight manner,

providing more gradual assurance. Unfortunately, the testing and

proof communities have historically been largely disjoint, and much

of the existing work in these areas focuses on a single approach and

tool.

We propose a more flexible use of rich specifications, via a single

language for specifications; these can be refined as they are written

using feedback from testing and property-based testing, and can

eventually be used for proof, if desired [1]. We demonstrate our

approach by applying this workflow to critical systems software

written in C, using separation logic to capture the complex ownership

properties present in such code. Concretely, we use the CN [2]

separation-logic specification language; the Fulminate [3] runtime

testing tool, which translates CN specifications into C runtime

checks and checks ownership dynamically; the Darcy [1]

property-based testing tool, which generates random

precondition-satisfying inputs to drive Fulminate assertions; and

the CN proof tool. In this talk, I will discuss our experience applying

this testing-first workflow to a fragment of real-world systems code

(Google's pKVM hypervisor); our work in getting the

Fulminate-instrumented fragment running baremetal at the

hypervisor privilege level as part of pKVM; and provide an overview of

the tools we developed and improved in service of these.

[1] Code-Specify-Test-Debug-Prove: Flexibly Integrating

Separation Logic Specification into Conventional Workflows. Zain K

Aamer*, Rini Banerjee*, Hiroyuki Katsura*, David

Kaloper-Meršinjak*, Dimitrios J. Economou, Kayvan Memarian, Dhruv

Makwana, Neel Krishnaswami, Benjamin C Pierce, Christopher Pulte,

Peter Sewell. To appear in PLDI 2026. *authors contributed equally

[2] CN: Verifying Systems C Code with Separation-Logic Refinement

Types. Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan

Memarian, Peter Sewell, Neel Krishnaswami. POPL 2023.

[3] Fulminate: Testing CN Separation-Logic Specifications in C. Rini

Banerjee, Kayvan Memarian, Dhruv Makwana, Christopher Pulte, Neel

Krishnaswami, and Peter Sewell. POPL 2025.