Download: PDF, slides (PDF), Verdi website, Verdi implementation, Raft implementation and proofs.
“Planning for change in a formal verification of the Raft consensus protocol” by Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson. In CPP 2016: 5th ACM SIGPLAN Conference on Certified Programs and Proofs, (St. Petersburg, FL, USA), Jan. 2016, pp. 154-165.
We present the first formal verification of state machine safety for the Raft consensus protocol, a critical component of many distributed systems. We connected our proof to previous work to establish an end-to-end guarantee that our implementation provides linearizable state machine replication. This proof required iteratively discovering and proving 90 system invariants. Our verified implementation is extracted to OCaml and runs on real networks.
The primary challenge we faced during the verification process was proof maintenance, since proving one invariant often required strengthening and updating other parts of our proof. To address this challenge, we propose a methodology of planning for change during verification. Our methodology adapts classical information hiding techniques to the context of proof assistants, factors out common invariant-strengthening patterns into custom induction principles, proves higher-order lemmas that show any property proved about a particular component implies analogous properties about related components, and makes proofs robust to change using structural tactics. We also discuss how our methodology may be applied to systems verification more broadly.
Download: PDF, slides (PDF), Verdi website, Verdi implementation, Raft implementation and proofs.
BibTeX entry:
@inproceedings{WoosWATEA2016,
author = {Doug Woos and James R. Wilcox and Steve Anton and Zachary
Tatlock and Michael D. Ernst and Thomas Anderson},
title = {Planning for change in a formal verification of the {Raft}
consensus protocol},
booktitle = {CPP 2016: 5th ACM SIGPLAN Conference on Certified Programs
and Proofs},
pages = {154-165},
address = {St.\ Petersburg, FL, USA},
month = jan,
year = {2016}
}
(This webpage was created with bibtex2web.)
Back to Michael Ernst's publications.