JULY 2017 | VOL. 60 | NO. 7 | COMMUNICATIONS OF THE ACM 91
implementation in a simplified environment into an equivalent implementation that is robust in a more hostile
environment, offering a clean approach to composition.
Unlike IronRSL, Verdi does not prove any liveness properties and its current implementation of Raft does not support verified marshalling and parsing, state transfer, log
truncation, dynamic view-change timeouts, a reply cache,
8. SUMMARY AND FUTURE WORK
The IronFleet methodology slices a system into specific
layers to make verification of practical distributed system
implementations feasible. The high-level spec gives the
simplest description of the system’s behavior. The protocol layer deals solely with distributed protocol design; we
connect it to the spec using TLA+ 13 style verification. At the
implementation layer, the programmer reasons about a
single-host program without worrying about concurrency.
Reduction and refinement tie these individually feasible
components into a methodology that scales to practically-sized concrete implementations. This methodology admits
conventionally structured implementations capable of
processing up to 18,200 requests/s (IronRSL) and 28,800
requests/s (IronKV), performance competitive with unverified reference implementations.
In the future, we plan to address two of IronFleet’s
limitations. First, the performance of even state-of-the-art verification tools limits the scale of the systems we
can easily verify. For instance, for every system invariant, we must prove that no action can invalidate that
invariant. Automated reasoning handles this with little
developer burden when there are tens of actions, but
likely not when there are thousands. To fix this, we will
require stronger modularity, for example, to enable efficient verification that one component’s actions do not
interfere with another component’s invariants. Another
limitation of IronFleet is that it allows concurrency only
among processes, not among threads that share memory.
The software verification community provides a variety of
approaches, such as ownership and separation logic, to
address this problem. We plan to make such approaches
practical in the context of automated verification of large-scale systems.
overhead to enforce type safety on code that provably
does not need it.
7. RELATED WORK
The recent increase in the power of software verification has
emboldened several research groups to use it to prove the
correctness of single-machine implementations, for example, the seL4 microkernel. 10 Our Ironclad project6 shows
how to completely verify the security of sensitive services all
the way down to the assembly code.
Distributed systems are known to harbor subtle design
and implementation errors. Researchers have recently
started generating machine-checkable proofs of correctness
for their protocols, since paper proofs, no matter how formal, can contain serious errors. 25 In some cases, the proof of
correctness encompasses the implementation, as well. In all
cases, the systems proven correct have been much smaller
and simpler than ours.
Ridge21 proves the correctness of a persistent message
queue; however, his system is substantially smaller in
scale than ours and has no proven liveness properties.
Schiper et al. 22 verify the correctness, but no liveness
properties, of a Paxos implementation. However, they
do not verify the state machine replication layer of this
Paxos implementation, only the consensus algorithm,
ignoring complexities such as state transfer. In contrast
to IronFleet, which exploits multiple levels of abstraction
and refinement, their approach posits a language below
which all code generation is automatic, and above which
a human can produce a one-to-one refinement. It is
unclear if this approach will scale up to complex distributed systems.
Verdi23, 24 implements verified distributed systems.
Its verified system transformers convert a developer’s
1. Bolosky, W. J., Douceur, J. R., Howell, J.
The Farsite project: a retrospective.
ACM SIGOPS Oper. Syst. Rev. 41, 2
(Apr. 2007), 17–26.
2. de Moura, L. M., Bjørner, N. Z3:
An efficient SM T solver. In
Proceedings of the Conference
on Tools and Algorithms for the
Construction and Analysis of
3. Detlefs, D., Nelson, G., Saxe, J.B.
Simplify: A theorem prover for
program checking. J. ACM 52 (2003),
4. Fischer, M.J., Lynch, N.A., Paterson, M.S.
Impossibility of distributed
consensus with one faulty process.
J. ACM 32, 2 (Apr. 1985), 374–382.
5. Floyd, R. Assigning meanings to
programs. In Proceedings of Symposia
in Applied Mathematics (1967).
American Mathematical Society,
6. Hawblitzel, C., Howell, J., Lorch, J. R.,
Narayan, A., Parno, B., Zhang, D.,
Zill, B. Ironclad apps: End-to-end
security via automated full-system
verification. In Proceedings of
USENIX OSDI (Oct. 2014).
7. Hoare, T. An axiomatic basis for
computer programming. Commun.
ACM 12 (1969), 576–580.
8. Joshi, R., Lamport, L., Matthews, J.,
Tasiran, S., Tuttle, M., Yu, Y. Checking
cache coherence protocols with
TLA+. J. Formal Methods Syst. Des.
22, 2 (2003), 125–131.
9. Killian, C. E., Anderson, J. W., Braud, R.,
Jhala, R., Vahdat, A.M. Mace:
Language support for building
Figure 10. IronKV’s performance is competitive with Redis, an
unverified key-value store. Results averaged over three trials.
8KB 128B 1KB
c ) IronRSL
Figure 9. IronRSL’s performance is competitive with an unverified
MultiPaxos system. Results averaged over three trials.