It is a truth universally acknowledged that critical real-world systems infrastructure must be in want of high assurance. The slope to high assurance is an infamously steep one, however, with full functional correctness verification efforts for systems software having historically taken years to complete. In order to verify such software, one must first \emph{write specifications} that capture its full behaviour, and in the context of systems software, this includes not only functional properties but also those of ownership. Writing such specifications is an innately challenging task, even for formal methods experts; this is because: (1) as the size and complexity of the specification grows, proof has a tendency to become unusably slow (with even state-of-the-art tools taking several hours to provide a result to the user), making incremental specification-writing very challenging; and (2) although specifications are modular in that they can be written and proved on a per-function basis, one must write a \emph{full} specification (with precondition, postcondition, loop invariants, lemmas, etc) to have a chance of proving the function correct at all. It is clear that there are many stages of the specification-writing process where the user would benefit from some lightweight assurance of both the software they are checking and the specifications themselves.

One way to achieve such gradual assurance is to \emph{test} specifications as they are being written. This approach presents a number of benefits: (1) testing is much faster than proof, and can immediately find mistakes in both the specifications and the software being checked; and (2) testing does not require the user to have written a complete specification – in fact, one could start by writing simple inline assertions, perhaps only capturing functional behaviour, and work their way up to richer specifications that describe more complex properties such as those of ownership – and so specification bugs can be caught earlier in this process of writing \emph{partial} specifications. Crucially, this approach provides an on-ramp to full functional correctness verification, with an important off-shoot being that the same specifications can be used for both testing \emph{and} proof. This idea is not a new one, but we argue that it is underappreciated in the field of verification as a whole.

In the context of gaining assurance of real-world systems infrastructure, we note that applying this idea in practice is no small feat. While there have been significant efforts to verify systems software over the past few decades, much of it has been focused on either developing formalisation-friendly implementations from the ground up, or has targeted idealised subsets of low-level programming languages such as C. Formally specifying and verifying pre-existing, idiomatic, real-world C code remains an elusive and challenging research problem for a number of reasons, including the complexity of its semantics (e.g. undefined behaviours, complex control-flow, implicit type coercions) and that of its typical ownership patterns, which are ubiquitous in conventional systems code. Separation logic has become a highly important tool for tackling the latter, providing a means to formally capture the complex ownership properties of low-level imperative programs, and has been used as the basis for a number of proof and industrial static analysis tools in recent years. However, it has rarely been used for testing until recently, for both technical and (we would argue) social reasons.

In this talk, we discuss our ongoing work in using separation-logic tools to retroactively gain assurance of real-world systems software written in C. For this purpose, we have used CN, a state-of-the-art separation-logic verification tool for C; Fulminate, a tool that translates CN separation-logic specifications into runtime-checkable C assertions; and Bennet, a property-based testing tool that generates sophisticated random inputs using the provided CN specifications to exercise Fulminate-instrumented C files. We discuss the various improvements we have made to each of these tools in order to facilitate applying them in tandem to a fragment of Google’s pKVM hypervisor, known as the heap allocator; our experience in writing CN specifications for the heap allocator and testing them \emph{as they were being written}; and our efforts in getting a Fulminate-instrumented version of this to run within pKVM at the privileged Arm Exception Level 2 (EL2).