Systems code is challenging to verify, because it uses constructs (like raw pointers, pointer arithmetic, and bit twiddling) that are hard for tools to reason about. Existing approaches either sacrifice programmer friendliness, by demanding significant manual effort and verification expertise, or generality, by restricting the programming language or requiring that the code adapt to the verification tool.

We identify a new point in the design space of verifiers that enables a different set of trade-offs, which prove practical in the context of verifying critical system-components. We use several novel techniques to develop the TPot verification framework, targeted specifically at systems code written in C. With TPot, developers verify critical components they implement in standard, unrestricted C, using a C-based language to write “proof-oriented tests” (POTs) that specify the desired behavior. TPot then runs the POTs to prove correctness. We evaluate TPot on 6 different systems-code bases, and show that it can verify them at the same level as 4 state-of-the-art verifiers, while reducing the annotation burden by a factor of 1.36-3.46x. TPot does not require these code bases to be adapted for verification and achieves verification times compatible with typical continuous-integration workflows.

The process isolation enforceable by commodity hardware and operating systems is too weak to protect secrets from malicious code running on the same machine: Spectre-era attacks exploit timing side channels derived from contention on shared microarchitectural resources to extract secrets. With appropriate hardware support, however, we can construct isolated enclaves and safeguard independent processes from interference through timing side channels, a necessary step towards integrity and confidentiality guarantees.

In this paper, we describe our work on formally specifying and verifying that a synthesizable hardware architecture implements strong timing isolation for enclaves. We reason about the cycle-accurate semantics of circuits with respect to a trustworthy formulation of strong isolation based on “air-gapped machines” and develop a modular proof strategy that sidesteps the need to prove functional correctness of processors. We apply our method on a synthesizable, multicore, pipelined RISC-V design formalized in Coq.

Modern software needs fine-grained compartmentalization, i.e., intra-process isolation. A particularly important reason for it are supply-chain attacks, the need for which is aggravated by modern applications depending on hundreds or even thousands of libraries. Object capabilities (ocaps) are a particularly salient approach to compartmentalization, but they require the entire program to assume a lack of ambient authority. Most of existing code was written under no such assumption; effectively, existing applications need to undergo a rewrite-the-world migration to reap the advantages of ocap. We propose gradual compartmentalization, an approach which allows gradually migrating an application to object capabilities, component by component in arbitrary order, all the while continuously enjoying security guarantees. The approach relies on runtime authority enforcement and tracking the authority of objects the type system. We present Gradient, a proof-of-concept gradual compartmentalization extension to Scala which uses Enclosures and Capture Tracking as its key components. We evaluate our proposal by migrating the standard XML library of Scala to Gradient.

We present an executable, proven-safe, faithful, and future-proof Coq mechanization of JavaScript regular expression (regex) matching, as specified by the last published edition of ECMA-262 section 22.2. This is, to our knowledge, the first time that an industrial-strength regex language has been faithfully mechanized in an interactive theorem prover. We highlight interesting challenges that arose in the process (including issues of encoding, corner cases, and executability), and we document the steps that we took to ensure that the result is straightforwardly auditable and that our understanding of the spec aligns with existing implementations.

We demonstrate the usability and versatility of the mechanization through a broad collection of analyses, case studies, and experiments: we prove that JavaScript regex matching always terminates and is safe (no assertion failures); we identify subtle corner cases that led to mistakes in previous publications; we verify an optimization extracted from a state-of-the-art regex engine; we show that some classic properties described in automata textbooks and used in derivatives-based matchers do not hold in JavaScript regexes; and we demonstrate that the cost of updating the mechanization to account for changes in the original specification is reasonably low.

Our mechanization can be extracted to OCaml and linked with Unicode libraries to produce an executable engine that passes the relevant parts of the official Test262 conformance test suite.

Modern regex languages have strayed far from well-understood traditional regular expressions: they include features that fundamentally transform the matching problem. In exchange for these features, modern regex engines at times suffer from exponential complexity blowups, a frequent source of denial-of-service vulnerabilities in JavaScript applications. Worse, regex semantics differ across languages, and the impact of these divergences on algorithmic design and worst-case matching complexity has seldom been investigated.

This paper provides a novel perspective on JavaScript's regex semantics by identifying a larger-than-previously-understood subset of the language that can be matched with linear time guarantees. In the process, we discover several cases where state-of-the-art algorithms were either wrong (semantically incorrect), inefficient (suffering from superlinear complexity) or excessively restrictive (assuming certain features could not be matched linearly). We introduce novel algorithms to restore correctness and linear complexity. We further advance the state-of-the-art in linear regex matching by presenting the first nonbacktracking algorithms for matching lookarounds in linear time: one supporting captureless lookbehinds in any regex language, and another leveraging a JavaScript property to support unrestricted lookaheads and lookbehinds. Finally, we describe new time and space complexity tradeoffs for regex engines. All of our algorithms are practical: we validated them in a prototype implementation, and some have also been merged in the V8 JavaScript implementation used in Chrome and Node.js.

We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve cryptography. We used very different formal-reasoning techniques throughout the stack, ranging from computer algebra, symbolic execution, and verification-condition generation to interactive verification of a compiler for a C-like language. All these component specifications and domain-specific reasoning techniques are defined and justified against common foundations in the Coq proof assistant. Common between these components is a minimalistic specification style based on functional programs operating on simple objects, omnisemantics for program execution, and assertions in simple separation logic. This design enables us to bring the components together in a top-level correctness theorem that can be audited without understanding or trusting the internal interfaces and tools. Our case study is a simple cryptographic server for flipping of a bit of state through authenticated network messages, and the proof about it shows total functional correctness including static bounds about memory usage. We believe it is the first formal verification covering a full software stack that models both network input and output. This paper also describes our experiences with the specific verification tools we build upon, along with detailed analysis of reasons behind the widely varying levels of productivity we experienced between combinations of tools and tasks.

There are typically two ways to compile and run a purely functional program verified using an interactive theorem prover (ITP): automatically extracting it to a similar language (typically an unverified process, like Coq to OCaml) or manually proving it equivalent to a lower-level reimplementation (like a C program). Traditionally, only the latter produced both excellent performance and end-to-end proofs.

This paper shows how to recast program extraction as a proof-search problem to automatically derive correct-by-construction, high-performance code from purely functional programs. We call this idea relational compilation — it extends recent developments with novel solutions to loop-invariant inference and genericity in kinds of side effects.

Crucially, relational compilers are incomplete, and unlike traditional compilers, they generate good code not because of a fixed set of clever built-in optimizations but because they allow experts to plug in domain–specific extensions that give them complete control over the compiler's output.

We demonstrate the benefits of this approach with Rupicola, a new compiler-construction toolkit designed to extract fast, verified, idiomatic low-level code from annotated functional models. Using case studies and performance benchmarks, we show that it is extensible with minimal effort and that it achieves performance on par with that of handwritten C programs.

Highly automated theorem provers like Dafny allow users to prove simple properties with little effort, making it easy to quickly sketch proofs. The drawback is that such provers leave users with little control about the proof search, meaning that the small changes inherent to the iterative process of writing a proof often lead to unpredictable variations in verification time, and eventually hard-to-diagnose proof failures. This sometimes turns the boon of high automation into a curse, as instead of breaking early and showing unsolved goals to the user like in Coq, proofs tend to gradually become unstable until their verification time explodes. At this point, the absence of a proof context to investigate often leaves the user to a painful debugging session. In this paper, we show how to use Dafny modules to encode Coq-like induction principles to dramatically improve the stability and maintainability of proofs about inductive data structures.

Diagrams are ubiquitous in the development and presentation of proofs, yet surprisingly uncommon in computerized mathematics. Instead, authors and developers rely almost exclusively on line-oriented notations (textual abbreviations and symbols). How might we enrich interactive theorem provers with on-the-fly visual aids that are just as usable? We answer this question by identifying a key challenge: designing declarative languages for composable diagram templates, that provide good-looking implementations of common patterns, and allow for rapid prototyping of diagrams that remain stable across transformations and proof steps.

The process isolation enforceable by commodity hardware is too weak to protect secrets from malicious code running on the same machine: Spectre-era attacks have exploited timing side channels derived from contention on shared microarchitectural resources to extract secrets. We describe our work in progress on specifying and verifying strong timing isolation for synthesizable hardware. We reason about the cycle-accurate semantics of circuits with respect to a trustworthy formulation of strong isolation based on “air-gapped machines” and develop a modular proof strategy that sidesteps the need to prove functional correctness of processors. We demonstrate our method on a multicore, pipelined, RISC-V design formalized in Coq. Finally, we discuss future directions toward composing isolation guarantees with speculative, constant-time guarantees to obtain a software-to-hardware, end-to-end guarantee of timing side channel freedom.