Chennai Mathematical Institute

Seminars




CS Faculty Talks
Date: Monday, 7 October 2024
Time: 03:00 - 03:50 PM
Venue: Seminar Hall
Formal Verification of Pipelined Moonshot State Machine Replication Protocol

M Praveen
Chennai Mathematical Institute.
07-10-2024


Abstract

Suppose a collection of servers is striving to maintain an artifact similar to a bank ledger, consisting of a sequence of transactions. Each server must be able to add transactions, and all servers must have the same sequence of transactions. All this have to be achieved without any one server being designated as central authority. A state machine repli- cation protocol is a set of fixed rules about how servers communicate among themselves to achieve this. Pipelined Moonshot is such a proto- col, recently proposed to optimally utilize communication bandwidth. Many such protocols have been proposed, with bugs being discovered in some of them, many years after they appeared in peer reviewed publi- cation platforms. This talk describes a project we did for the company which designed the Pipelined Moonshot protocol, to formally verify its correctness. We describe the underlying principles of how such cor- rectness criteria can be formulated as logical statements and how their correctness can be (dis)proved using solvers. The talk will be at an introductory level and no background is necessary in either logic or distributed protocols.