Formal Verification of a Distributed Dynamic Reconfiguration Protocol (CPP 2022)

Sun 16 - Fri 28 January 2022 Philadelphia, Pennsylvania, United States

Who

William Schultz, Ian Dardik, Stavros Tripakis

Track

CPP 2022

Time Zone

The program is currently displayed in (GMT-05:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

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

Abstract

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.

Link to Preprint

https://arxiv.org/abs/2109.11987

William Schultz

Northeastern University

Ian Dardik

Northeastern University

Stavros Tripakis

Northeastern University

Time Zone

The program is currently displayed in (GMT-05:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

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