Communications of the ACM

practical systems can be built from existing verified components, eliminating entire classes of bugs—from the hardware up to the application logic.

Verified Compilers: Compcert

Leroy, X.

Formal verification of a realistic compiler.

Communications of the ACM 52, 7 (July

2009), 107–115; https://cacm.acm.org/ magazines/2009/7/32099-formal-verification- of-a-realistic-compiler/abstract

Compiler bugs are infectious: A buggy compiler can make otherwise correct source programs misbehave at runtime. This is concerning for any programmer, but especially so if the programmer wants to reason at the source level or use source-level program analysis. Any analysis results are at risk of being invalidated by the compiler’s disease.

CompCert is a C compiler that has been formally proven never to miscompile source programs. More precisely, CompCert is guaranteed to produce assembly code that is equivalent to the C source program. CompCert is programmed and proved using the Coq proof assistant.

Like all verified systems, CompCert trusts certain other pieces of software to be correct. The TCB of a verified system generally includes tools used to carry out the verification, the specification, and the shim, or glue code, used to connect the system to the rest of the world. CompCert’s TCB contains tools such as Coq itself, the OCaml compiler and runtime, and the operating system; the specification, including the semantics of both C and the target assembly language; and its shim, which is an unverified OCaml program responsible for reading files from disk and so on.

Verified Operating Systems: seL4

Klein, G., et al. seL4: Formal verification of an operating-system kernel. Communications of the ACM

53, 6 (June 2010), 107–115; http://dl.acm.org/ citation.cfm?id=1743574

Operating-systems bugs, like compiler bugs, may cause a correct program to misbehave. Even worse, the OS strain of contagious bugs can result in unintended interaction among processes.

Such interaction can lead to security
holes, such as leaks of sensitive data
across process boundaries.
seL4 is an operating-system ker-
nel that is verified for full functional
correctness. More precisely, seL4 is
shown to refine an abstract specifi-
cation of its behavior. This refine-
ment guarantees, among other
things, that no system calls ever pan-
ic unexpectedly, loop infinitely, or
return wrong results. These guaran-
tees are sufficient to establish secu-
rity properties such as access control
and process isolation.
The refinement proof, done in the
Isabelle/HOL proof assistant, first
shows that the C implementation re-
fines an executable specification writ-
ten in Haskell; the Haskell specifica-
tion is then shown to refine the
abstract specification.

seL4’s TCB includes Isabelle/HOL itself, the C compiler, the hardware, the abstract specification, and the shim, which consists of several hundred lines of handwritten assembly.

Verified Distributed Systems: Verdi Wilcox, J.R., et al.

Verdi: A framework for implementing and formally verifying distributed systems. In Proceedings of the Conference on Programming Language Design and Implementation, 2015; http://homes. cs.washington.edu/~mernst/pubs/verify- distsystem-pldi2015-abstract.html

At least compiler and operating-system bugs are localized on a particular node. In contrast, avoiding distrib-uted-systems bugs requires reasoning about the interaction between nodes. Furthermore, distributed systems must tolerate failure of the underlying hardware.

Verdi supports reasoning about distributed systems by modeling the network using network semantics, which formally capture the potential faults the nodes might experience, including dropped messages, crashing machines, and so on. Verdi employs verified systems transformers (VSTs), which can, for example, add fault tolerance to existing systems. Verdi has been used to verify the Raft consensus protocol as a VST from a single node to a replicated system.

Verdi trusts Coq itself, the OCaml compiler and runtime, the fact that the network obeys the fault model, and its shim, which is an unverified OCaml program responsible for low-level network and disk access.

Future Directions

The research community has now verified many pieces of common infrastructure. Going forward, how do we connect these pieces to build larger verified applications?

As a simple example, imagine combining verified systems from the domains highlighted here to build a verified replicated key-value store. Such a system would use Raft for replication; be compiled with a verified compiler; and run on a verified operating system. Today, it is not clear how to execute such a plan for several reasons.

First, the systems are written in different proof assistants—CompCert and Verdi in Coq, seL4 in Isabelle/ We need techniques to build larger verified systems from verified components. One bright spot on this horizon is the recent DeepSpec project, which seeks to connect verification projects across many abstraction layers. Future work should seek to integrate verified systems into a library of reliable components that can be snapped together to build bug-free applications. The existence of such a library will also lower the barrier to entry for verifying systems, eventually leading to a world where it is no more expensive to verify a system than to test it thoroughly.

Albert Kwon is a Ph. D. candidate in the EECS department at MIT, where he has worked on oblivious RAMs, public key infrastructure, cryptocurrencies, anonymous reputation, and anonymous communication networks. James R. Wilcox is a Ph. D. student at the University of Washington in the Programming Languages and Software Engineering lab ( http://uwplse.org/).