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.

Professor J Strother Moore, University of Texas at Austin, USA

Professor J Strother Moore, University of Texas at Austin, USA

J Strother Moore held the Admiral B.R. Inman Centennial Chair in Computing Theory at the University of Texas at Austin until his retirement in 2015. He is the author of many books and papers on automated theorem proving and mechanical verification of computing systems. Along with Boyer he is a co-author of the Boyer-Moore theorem prover and the Boyer-Moore fast string searching algorithm. With Matt Kaufmann he is the co-author of the ACL2 theorem prover. In 1999, Boyer and Moore were awarded the Herbrand Award for their work in automatic theorem proving. Boyer, Moore, and Kaufmann were awarded the 2005 ACM Software Systems Award for the Boyer-Moore theorem prover. Moore is a Fellow of the American Association for Artificial Intelligence, the ACM, the Royal Society of Edinburgh (Corresponding Fellow), and the US National Academy of Engineering.

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.

Professor Kathleen Fisher, Tufts University, USA

Professor Kathleen Fisher, Tufts University, USA

Kathleen Fisher is Professor in the Computer Science Department at Tufts University. Previously, she was a Principal Member of the Technical Staff at AT&T Labs Research, a Consulting Faculty Member in the Computer Science Department at Stanford University, and a program manager at DARPA where she started and managed the HACMS and PPAML programs. Kathleen's research focuses on advancing the theory and practice of programming languages and on applying ideas from the programming language community to the problem of ad hoc data management. The main thrust of her work has been in domain-specific languages to facilitate programming with massive amounts of ad hoc data.  Kathleen is an ACM Fellow. She has served as program chair for FOOL, ICFP, CUFP, and OOPSLA and as general chair for ICFP. Kathleen is past Chair of the ACM Special Interest Group in Programming Languages (SIGPLAN), past Co-Chair of CRA's Committee on the Status of Women (CRA-W), a former editor of the Journal of Functional Programming, and an associated editor of TOPLAS. Kathleen is a recipient of SIGPLAN’s Distinguished Service Award.

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.

Neil White, Altran, UK

Neil White, Altran, UK

Neil White is the Head of Engineering for Altran UK. He has worked in the area of bespoke safety-critical software for nearly 20 years. In that time he has delivered signature projects into a variety of markets, including Air Traffic Control, Aerospace, Defence, and Finance. His projects have included the first deployments to new regulatory standards, and the industrial introduction of new technologies. He is a long-term proponent of formal methods and demonstrably correct systems. He is currently interested in the sustainable evolution required to keep hi-tec companies at the forefront of their markets.

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.

Professor Daniel Kroening, University of Oxford, UK

Professor Daniel Kroening, University of Oxford, UK

Daniel Kroening received the M.E. and doctoral degrees in computer science from the University of Saarland, Saarbrucken, Germany, in 1999 and 2001, respectively. He joined the Model Checking group in the Computer Science Department at Carnegie Mellon University, Pittsburgh PA, USA, in 2001 as a Post-Doc. He was an assistant professor at the Swiss Technical Institute (ETH) in Zurich, Switzerland, from 2004 to 2007. He is now Professor of Computer Science at the University of Oxford. His research interests include automated formal verification of hardware and software systems, concurrency, decision procedures, embedded systems and hardware/software co-design.

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.

Professor Gerwin Klein, Data61 and UNSW Australia, Australia

Professor Gerwin Klein, Data61 and UNSW Australia, Australia

Gerwin Klein is a Senior Principal Researcher at Data61 (previously NICTA), and Conjoint Professor at UNSW in Sydney, Australia. He is leading Data61's Formal Methods research in the Trustworthy Systems Group and is the leader of the seL4 verification effort that created the first machine-checked proof of functional correctness of a general-purpose microkernel. He joined NICTA in 2003 after receiving his PhD from Technische Universität München, Germany, where he formally proved type-safety of the Java Bytecode Verifier in the theorem prover Isabelle/HOL. His research interests are in interactive formal verification, programming languages, and systems code. Gerwin Klein has won a number of awards, among them together with his team the 2011 MIT TR-10 award for the top ten emerging technologies world-wide.

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.

Professor Nickolai Zeldovich, MIT CSAIL, USA

Professor Nickolai Zeldovich, MIT CSAIL, USA

Nickolai Zeldovich is an Associate Professor at MIT's department of Electrical Engineering and Computer Science, and a member of the Computer Science and Artificial Intelligence Laboratory. His research interests are in building practical secure systems, from operating systems and hardware to programming languages and security analysis tools. He received his PhD from Stanford University in 2008, where he developed HiStar, an operating system designed to minimize the amount of trusted code by controlling information flow. In 2005, he co-founded MokaFive, a company focused on improving desktop management and mobility using x86 virtualization. His current research is focused on formal verification of systems software.

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.

Dr Mark Batty, University of Kent, UK

Dr Mark Batty, University of Kent, UK

Mark Batty is an expert on language concurrency models. Prior to his work, C and C++ did not have a well-defined concurrency model; Batty worked with the ISO on the 2011 language revisions to define a rigorous formal model in tight correspondence with the standard. In the process, he identified major problems, proposing fixes that were adopted prior to ratification; a rare example of formal semantics directly impacting mainstream industrial practice. With others, Batty proved-sound proposed industry-standard compiler mappings from C++11 to x86 and Power, he proved (in HOL4) that simple race-free programs have SC behaviour (DRF-SC), a central tenet of the design, and he defined a sound principle for compositional reasoning in C++11. Despite these positive results, Batty showed that C/C++11 has fundamental problems: to admit compiler optimisations, the semantics has been made too weak. Batty's recent work focuses on GPGPU concurrency: he has identified bugs in a nascent AMD GPU design feature and worked with Nvidia on their internal specifications.