Lennart Beringer is an Associate Research Scholar at Princeton University, where he uses interactive proof assistants to develop provably correct compilers, program analyses, and other software verification tools. Previously, he held research appointments at the Ludwig-Maximilians-University Munich and the University of Edinburgh, where he developed proof-carrying-code techniques for mobile code architectures, focusing on properties of resource consumption and information flow security. He received his PhD degree from the University of Edinburgh for a language-based analysis of an idealized asynchronous processor architecture. In 2012, he served as the co-chair of the Third International Conference on Interactive Theorem Proving (ITP).
Luke Muehlhauser: One of the projects to which you contribute is the Verified Software Toolchain. How would you summarize what has been achieved so far? What do you hope to have achieved in the next year or two on that project?
Lennart Beringer: The Verified Software Toolchain is a collection of verification tools for the C programming language, implemented and formally verified in the Coq proof assistant, with a connection to the formally verified CompCert compiler developed by Xavier Leroy at INRIA, France.
The heart of the VST is a Hoare-style program logic suitable for verifying partial-correctness properties and program safety, i.e. the absence of abnormal program termination due to, e.g., an attempt to dereference a dangling pointer. Program specifications are written in a highly expressive variant of concurrent separation logic that supports higher-order reasoning, impredicative quantification, and other concepts necessary for formulating, e.g., the resource invariants of locks in POSIX-style multithreading.
In addition to the core program logic, the VST contains support for proof automation, and a verifiably sound implementation of a shape analysis, the two components of which — a symbolic execution engine and an entailment checker for the Smallfoot-fragment of separation logic — can be either code-extracted to yield stand-alone tools, or integrated into Coq- or Ocaml-based analyses, including Smallfoot itself. The proof automation component consists of various Coq tactics, auxiliary lemmas, and specification abstractions that capture typical proof patterns in concrete application programs. Special emphasis here is put on the idea of hierarchically organized layers of assertion formats that hide much of the complexity of the underlying logic from the user. An important goal of our current research is the discovery of additional such reasoning patterns for various programming and specification styles, and the exploitation of such structure to further enhance automation and performance. Regarding applications of the VST, we believe that in addition to the typical domains of high-assurance software, concrete open-source implementations of formal standards or libraries provide excellent case studies for evaluating further enhancements to the VST. At the same time, machine-checkable proofs (or even just precise specifications) of such libraries can contribute to the public level of trust that everyday users put on these libraries.
Many design decisions and implementation details of the VST are described in Andrew Appel’s recent book, Program Logics for Certified Compilers (CUP 2014), while the source code is publicly available here.
A further aspect of our work concerns CompCert itself. Here, we are collaborating with Leroy and others to evolve CompCert’s specification and proof to cover shared memory interaction between threads, and formal models of linking. Indeed, a modular notion of Compiler correctness should respect that communication with the OS, with libraries, or with separately compiled program modules in C crucially relies on exchanging pointers to buffers or other shared data structures. Instead, CompCert’s notion of compiler correctness employs a whole-program view of compilation. However, it is far from easy to reconcile pointer sharing with the requirements of typical compiler optimizations, as these routinely alter memory layout and eliminate or relocate existing pointers. In addition, compiler-managed memory locations such as return addresses and spilling locations must remain unmodified be even those external callees that have legitimate access to other stack-held data.
Luke: How would you describe the underlying motivation for the VST? How will the world be different for various kinds of programmers (and other actors) in 10 years if the VST continues to be funded and worked on at a good pace?
Lennart: Specifying the expected behavior of software, and verifying that concrete implementations satisfy these specifications, has been an active research area for several decades. But for many years, the effectiveness of program logics was limited, and one of the reasons for this was the lack of support for modular reasoning, particularly with respect to pointer sharing and data structures that are laid out in memory. About ten years ago, separation logics emerged as a promising technique to address this shortcoming, by allowing specifications and invariants to elegantly capture properties of the heap and other shared resources.
At the same time, interactive proof assistants (and the computation power of the underlying hardware) had sufficiently matured so that program logics could be effectively implemented, and could be equipped with machine-checkable proofs of soundness. Indeed, by developing CompCert, Leroy demonstrated that interactive theorem proving scales to real-world languages, and can cope with the complexity inherent in an industrial-strength optimizing compiler.
The VST project combines these two threads, while at the same time exploring how the current automation and specification boundaries can be pushed further.
The main tool chain of the VST will most likely be of interest to C programmers writing either high assurance software, to implementors of medium-scale software such as crypto libraries, or to developers using code synthesis techniques, where — instead of verifying the correctness of individually generated programs — one could envision verified synthesis tools that target the VST’s Clight program logic. Functional programmers may benefit by having a precise way to formally relate their high-level code written in Ocaml or Haskell to potentially more efficient code written in C, using Coq’s code extraction feature to mediate between these two worlds. By combining code extraction and compilation, it may even become possible to verify hybrid software systems in which some components are written in C and others in a functional language.
Another group of potential users is that of system designers: VST specifications enable individual components to be characterized by much richer interfaces than is possible using C header files or Java interfaces. As interfaces become more robust, truly component-oriented software development becomes possible, where adherence to specifications suffices to guarantee that substituting individual components does not have negative impact on global system properties.
For typical components of the standard system stack (OS, network protocols,…), such formally defined interfaces are in fact of interest in their own right, as the contract between, say, different components of the OS, the compiler, and the architecture, are notoriously difficult to comprehend. In addition to system developers and researchers, a third clientele may hence be that of educators, for whom specifications offer guidance for partitioning their material into self-contained, but interdependent units of teaching, and for explaining the mutual contracts and assumptions.
Luke: What are some other projects that seem to be aimed at similar goals but e.g. for other languages or via other approaches?
Lennart: I am not aware of other attempts to develop a similarly expressive program logic for a mainstream language, validate its soundness in a proof assistant, link it with a verified optimizing compiler, and equip it with sufficient proof automation to enable the verification of nontrivial programs.
However, many research groups address various subsets of these features.
Microsoft Research over the past decade developed an impressive collection of verification tools (VCC, Boogie/Dafny,…) which are primarily targeted at C#, but contain components or intermediate verification platforms that are also applicable to other programming languages. These have excellent proof automation, and are tightly integrated with modern SAT/SMT solvers, software model checkers, and other code analysis and inspection tools, but are not formally backed up by a machine-checkable soundness proof. At the same time, several groups within MSR already employ proof assistants to verify compilers, develop formal models of machine code, and validate program logics that are roughly comparable to the VST. It would hardly come as a surprise if these complementary research efforts were eventually integrated to yield an end-to-end machine-checkable toolchain for C#.
Chlipala’s Bedrock framework enables synthesis of verified assembly code by providing machine-checked code and specification patterns, enabling interaction between code fragments that deviates from C’s calling convention. In addition, this group pioneered proof engineering techniques that exploit advanced features of Coq’s tactic language and type theory, including some approaches we are now applying in the VST. We also incorporated ideas from Jesper Bengtson’s Charge! project, which provides a Coq-validated separation logic for Java.
Regarding compiler verification, Xavier Leroy and his collaborators at INRIA are extending CompCert towards full support for both C99 and C11, at the same time validating further optimization phases and – most recently – adding a verified parser.
UPenn’s Vellum project developed mechanized reasoning support for programs expressed in the LLVM intermediate representation, demonstrating that CompCert’s verification principles are also applicable to compiler infrastructures that were not designed with formal verification in mind, and to compilation based on static single assignment (SSA) in particular.
Closely related to compiler verification is the approach of translation validation – in fact, CompCert’s register allocator is also proved in this style. Recent contributions to mechanized translation validation include those by Sorin Lerner’s group at San Diego, and Greg Morrisett’s group at Harvard.
The development of practically validated, yet formally precise, mechanized specifications of real-world hard- and software systems, is an area that continues to grow, with recent examples including web servers, browsers, databases, operating system and hypervisors, relaxed memory models, and processor architectures. Particularly noteworthy are the projects under DARPA’s CRASH programme, as well as the REMS effort led by Peter Sewell at Cambridge (UK).
I probably failed to mention a number of projects, but I hope that the ones I mentioned give you a rough picture of the current developments.
Luke: Thanks, Lennart!
Did you like this post? You may enjoy our other Conversations posts, including:
