Verified trustworthy software systems

ACL2 has seen sustained use over the past decade or two at various companies including AMD, Centaur, Intel, Kestrel Institute, Oracle, and Rockwell-Collins. This paper focuses on how and why ACL2 is used in industry. The industrial applications of ACL2 include verification of the functional correctness of floating-point hardware designs in microcode, RTL, and Verilog, verification of other properties of such circuits, analysis of other transition systems including reactive systems and asynchronous transaction systems, basic results for elliptic curve cryptography, verification of information flow properties of operating systems, and modelling and verification of software in low level languages including machine code, microcode, JVM bytecode, and LLVM. ACL2 is well-suited to many of these applications because it is an integrated programming/proof environment supporting a subset of the ANSI standard Common Lisp programming language. As a programming language ACL2 permits the coding of efficient and robust programs; as a prover ACL2 can be fully automatic but provides many features permitting domain specific human-supplied guidance at various levels of abstraction. ACL2 specifications and models often serve as efficient execution engines for the modelled artefacts while permitting formal analysis and proof of properties. ACL2 also provides support for the development and verification of other formal analysis tools. However, ACL2 did not find its way into industrial use merely because of its technical features. The core ACL2 user/development community has a shared vision of making mechanised verification routine when appropriate and has been committed to this vision for the quarter century since the Computational Logic, Inc., Verified Stack. The community has focused on demonstrating the viability of the tool by taking on industrial projects (often at the expense of not being able to publish much) and is responsive to the needs of the industrial users in the community.

For decades, formal methods have offered the promise of software that doesn’t have exploitable bugs. Until recently, however, it hasn’t been possible to verify software of sufficient complexity to be useful. Recently, that situation has changed. SeL4 is an open-source operating system microkernel efficient enough to be used in a wide range of practical applications. It has been proven to be fully functionally correct, ensuring the absence of buffer overflows, null pointer exceptions, use-after-free errors, etc., and to enforce integrity and confidentiality properties. The CompCert Verifying C Compiler maps source C programs to provably equivalent assembly language, ensuring the absence of exploitable bugs in the compiler. A number of factors have enabled this revolution in the formal methods community, including increased processor speed, better infrastructure like the Isabelle/HOL and Coq theorem provers, specialised logics for reasoning about low-level code, increasing levels of automation afforded by tactic languages and SAT/SMT solvers, and the decision to move away from trying to verify existing artefacts and instead focus on co-developing the code and the correctness proof. In this talk I will explore the promise and limitations of current formal methods techniques for producing useful software that provably does not contain exploitable bugs. I will discuss these issues in the context of DARPA’s HACMS program, which has as its goal the creation of high-assurance software for vehicles, including quad-copters, helicopters, and automobiles.

In one sense, formal specification and verification has been highly successful: techniques have been developed in pioneering academic research, transferred to software companies through training and partnerships, and successfully deployed into systems with national significance. Altran UK have been in the vanguard of this movement and the talk will summarise some of the key deployments of formal techniques over the past 20 years. However, the impact of formal techniques remains within an industrial niche, and whilst government and OEMs across industry search for solutions to the problems of poor quality code, the wider software industry remain resistant to adoption of this proven solution. The talk will conclude by reflecting on some of the challenges we face as a community in ensuring that formal techniques achieve their true potential impact for society.

We show how a broad range of program analysis tasks can be solved using a second-order satisfiability solver, and present an instance of this approach that uses expression synthesis to solve quantified formulas with bit-vector constraints.

While many software systems are trusted, few are worthy of that trust. Formalproof, which can provide strong evidence for the highest levels of trustworthiness, is often discounted as infeasible for real software systems.

To show that this does not need to be the case, I will give an overview of the formal verification of the seL4 microkernel, from high-level classical security properties own to the binary code level. This verification was cheaper than current best practice industrial methods for achieving similar levels of assurance. However, it was still is more expensive than standard software construction, which delivers reasonable quality, albeit not high assurance. I will highlight our current research in proof engineering and code/proof co-generation to make deep formal software verification economically more viable for high-quality software.

FSCQ is the first file system with a machine-checkable proof (using the Coq proof assistant) that its implementation meets its specification and whose specification includes crashes.  FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero out directory blocks.  If a crash happens at an inopportune time, these bugs can lead to data loss.  FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover the file system correctly without losing data.

To state FSCQ's theorems, we introduce the Crash Hoare logic (CHL), which extends traditional Hoare logic with a crash condition, a recovery procedure, and logical address spaces for specifying disk states at different abstraction levels.  CHL also reduces the proof effort for developers through proof automation.  Using CHL, we developed, specified, and proved the correctness of the FSCQ file system.  Although FSCQ's design is relatively simple, experiments with FSCQ running as a user-level file system show that it is sufficient to run Unix applications with usable performance.  FSCQ's specifications and proofs required significantly more work than the implementation, but the work was manageable even for a small team of a few researchers.

Modern computer systems have intricate memory hierarchies that violate the intuition of a global timeline of interleaved memory accesses. In these so-called relaxed-memory systems, it can be dangerous to use intuition, specifications are universally unreliable, and the outcome of testing is both wildly nondeterministic and dependent on hardware that is getting more permissive of odd behaviour with each generation. These complications pervade the whole system, and have led to bugs in language specifications, deployed processors, compilers, and vendor-endorsed programming idioms – it is clear that current engineering practice is severely lacking.

I will describe my part of a sustained effort in the academic community to tackle these problems by applying a range of techniques, from exhaustive testing to mechanised formal specification and proof. I will focus on two cases of industrial impact: first, the formalisation, refinement and validation the 2011/14 C and C++ concurrency design, leading to changes in the ratified international standard, and second, an engagement with Nvidia, where I have helped to define and validate the relaxed memory model of their next generation of graphics processors. This work represents an essential enabling step for verification on modern concurrent systems.