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/).
Copyright held by authors/owners.
Publication rights licensed to ACM. $15.00.