CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016

We present the first formal verification of the Raft consensus protocol, a critical component of many distributed systems. We proved that our implementation is a linearizable replicated state machine, which required iteratively discovering and proving nSysInv system invariants. Our verified implementation can be extracted and run 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 imply 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.

Tue 19 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

14:00 - 15:30
Session 7: Verification for Concurrent and Distributed SystemsCPP at Room St Petersburg II
14:00
30m
Talk
Bisimulation Up-to Techniques for Psi-calculi
CPP
Johannes Å. Pohjola Uppsala University, Joachim Parrow Uppsala University
14:30
30m
Talk
Planning for Change in a Formal Verification of the Raft Consensus Protocol
CPP
Doug Woos University of Washington, James R. Wilcox University of Washington, Steve Anton University of Washington, Zachary Tatlock University of Washington, Seattle, Michael D. Ernst University of Washington, Thomas Anderson University of Washington
Pre-print
15:00
30m
Talk
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
CPP
Michel St-Martin University of Ottawa, Amy Felty University of Ottawa