S-REPLS 18

Systems software (e.g. operating systems, hypervisors) forms the foundation of all modern computing infrastructure, and so ensuring its reliability is critical, and various approaches have been explored over the past few decades in pursuit of this goal. Full functional correctness verification, although historically a slow process requiring specialist knowledge of proof tools, provides strong correctness guarantees by proving the absence of bugs for all possible executions. In the context of systems software, where a single bug that propagates up the stack can have far-reaching consequences, such guarantees are often not just desirable, but essential.

The majority of the overhead of such verification efforts lies in the process of writing explicit specifications that capture the full behaviour of the software to be verified. This includes function-level specifications like pre- and post-conditions, but also intermediate specifications like loop invariants. This process of writing specifications can be tedious at best, and inhibiting at worst: the feedback loop of writing a full specification, running a proof tool to check if it makes sense, and in the failure case, using the error message generated by the proof tool to debug the incorrect specification, is extremely slow and often unintuitive. Testing specifications concretely at runtime — as they are being written — is one way to alleviate these problems and provide more gradual assurance; testing makes discovering specification bugs easier and the specification-writing process more lightweight, making the checking and debugging of in-progress, partial specifications possible. In the context of testing and verifying systems code, we consider separation logic a crucial tool for capturing the complex ownership patterns that are prevalent in real-world systems programs. Separation-logic specification-testing has not been extensively explored until recently, for both technical and 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 performs dynamic ownership checking; and Darcy, a new property-based testing tool that generates sophisticated random inputs from the provided CN specifications to exercise Fulminate-instrumented C files. We discuss our experience in writing CN specifications for a fragment of Google’s pKVM hypervisor, the hyp allocator, and testing them as they were being written; our efforts in getting a Fulminate-instrumented version of the hyp allocator to run within pKVM at the privileged Arm Exception Level 2 (EL2); and the various improvements we have made to each of these tools to facilitate this work.

The classic algorithm for SAT solving, DPLL, runs in exponential time. The algorithm is entirely deterministic, except for choices about which variable to branch on and whether to try true or false first. This choice can be made deterministically using heuristics, but often randomness is employed. For the algorithm to find a solution in reasonable time, it must make only a small number of choices, although (thanks to backtracking) some of these may be wrong. By modelling the choices as nondeterminism, we obtain a declarative C SAT solver, executable using a SAT solver.

The declarative C SAT solver works using a bounded model checker to encode the problem of solving a SAT instance as a larger SAT instance, then using an existing SAT solver to resolve the nondeterminism. This is much less efficient than applying the existing SAT solver directly to the SAT instance of interest. However, by reframing SAT solving as an optimisation problem of minimising the amount of nondeterminism required, we can get an empirical measure of the hardness of an easy SAT instance, called a backdoor, which is more informative than syntactic measures such as number of variables or clauses.

Refinement types allow convenient automatic propagation of facts about values. However, refinement type systems are tricky: substituting a definition can break typeability, and soundness is highly sensitive to evaluation order. Dependent types are more robust, being insensitive to substitutions or evaluation order, but are less convenient. I'll show how, at least for linear rational arithmetic, the advantages of both can be combined. The key is to separate the predicate of a variable’s type (what it says about the value) from its projection (what it says about other variables), and to track all constraints in a single ordered context.

Unowned sharing, which is the use of an entity by more than one other entity without owning the shared entity, is ubiquitous in programming. We identify three sets of linguistic requirements for the practice of unowned sharing. The "stakeholder requirements" are those that enforce unownedness of the sharing and prevent duplication. The "coalition requirements" are those that pertain to the identification of an unowned sharing and programming in terms of it. Finally, there are also "practicality requirements."

We propose `unbound`s as a new programming construct that fulfills all those requirements. We demonstrate the suitability of `unbound`s for systems programming and their elegance by tackling three recurrent programming challenges: dependency injection, prevention of association bugs (i.e., those bugs caused due to the usage by what an entity is not conceptually associated with), and zero-boilerplate (de)serialization. Unsurprisingly, those three are all instances of unowned sharing. We discuss how `unbound`s support both family polymorphism and lightweight family polymorphism. An implementation of `unbound`s is available in Xlang, our new systems programming language.

Although software verification is key to reliability, the tools themselves are rarely validated due to the complexity of constructing effective test cases and oracles. Dr. Zhang will present systematic approaches to detect bugs in SMT solvers and verifiers, revealing thousands of critical bugs in the tools we trust. This talk will discuss the theoretical and practical implications of these findings and the latest advances.