Mon 17 Jan 2022 16:20 - 16:45 at Salon III - Security and Distributed Systems Chair(s): Alwyn Goodloe

We present a formal, machine checked TLA+ safety proof of MongoRaftReconfig, a distributed dynamic reconfiguration protocol. MongoRaftReconfig was designed for and implemented in MongoDB, a distributed database whose replication protocol is derived from the Raft consensus algorithm. We present an inductive invariant for MongoRaftReconfig that is formalized in TLA+ and formally proved using the TLA+ proof system (TLAPS). We also present a formal TLAPS proof of two key safety properties of MongoRaftReconfig, LeaderCompleteness and StateMachineSafety. To our knowledge, these are the first machine checked inductive invariant and safety proof of a dynamic reconfiguration protocol for a Raft based replication system.

Mon 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

15:30 - 17:10
Security and Distributed SystemsCPP at Salon III
Chair(s): Alwyn Goodloe NASA Langley Research Center
15:30
25m
Talk
Reflection, Rewinding, and Coin-Toss in EasyCryptRemote
CPP
Denis Firsov Tallinn University of Technology, Dominique Unruh University of Tartu
Pre-print Media Attached
15:55
25m
Talk
A verified algebraic representation of Cairo program executionRemote
CPP
Jeremy Avigad Carnegie Mellon University, USA, Lior Goldberg Starkware Industries Ltd., David Levit Starkware Industries Ltd., Yoav Seginer cdl-lang.org, Netherlands, Alon Titelman Starkware Industries Ltd.
Pre-print
16:20
25m
Talk
Formal Verification of a Distributed Dynamic Reconfiguration ProtocolInPerson
CPP
William Schultz Northeastern University, Ian Dardik Northeastern University, Stavros Tripakis Northeastern University
Pre-print
16:45
25m
Talk
Forward build systems, formallyInPerson
CPP
Sarah Spall Indiana University, Neil Mitchell Meta, Sam Tobin-Hochstadt Indiana University
Link to publication