View article

An instruction set architecture (ISA) is an abstract specification of the syntax and semantics of machine code. It defines an envelope of allowed behaviour for CPU designers and a set of assumptions that software designers can rely on. Instead of informal prose and pseudo-code [eg 1], rigorous, executable formalisations of ISAs disambiguate the contract and improve testability and support modification, experimentation and formal study [eg 3, 12, 19]. Such formalisations are a crucial requirement for formal verification of both hardware [eg 8] and software [eg 15]. We are interested in verifying that critical safety guarantees of the ISA are upheld by the semantics of all instructions. Our long-term goal is to verify security guarantees offered by ISAs, specifically features like Intel SGX [16], virtual memory or capability machines [6]. We want to verify these properties in a form that can be used to reason about programs, as a way to ultimately verify security properties of real systems. For achieving this, we take inspiration from recent formulations of capability safety in capability machines and high-level languages [10, 20, 22, 24]. Contrary to, for example, Nienhuis et al.[18], such techniques directly enable reasoning across encapsulation boundaries. These approaches use (essentially) a general purpose program logic, and formulate capability safety as a universal contract that automatically holds for arbitrary programs. The universal contract expresses guarantees provided by the machine and can be used for manually verifying trusted programs that interact with untrusted programs. We believe that this approach generalises well beyond capability safety …