Epistemic Model Checking and Synthesis of Byzantine Agreement Protocols

22^nd October 2024, 13:00 Ashton Lecture Theatre
Ron van der Meyden
University of New South Wales

Abstract

Logics of knowledge and knowledge-based programs provide a way to give
abstract descriptions of solutions to problems in fault-tolerant
distributed computing, and have been used to derive optimal protocols
for these problems with respect to a variety of failure
models. Generally, these results have involved complex pencil and
paper analyses with respect to the theoretical ``full-information
protocol" model of information exchange between network nodes. It is
equally of interest to be able to establish the optimality of
protocols using weaker, but more practical, models of information
exchange, or else identify opportunities to improve their performance.
Over the last 20 years, automated verification and synthesis tools for
the logic of knowledge have been developed, such as the model checker
MCK, that can be applied to this problem.

The talk will describe the application of MCK to automated analyses of
this kind. A number of information-exchange models are considered,
for the problems of Eventual and Simultaneous Byzantine Agreement
under a range of failure types. MCK is used to automatically analyze
these models. The results demonstrate that it is possible, for small
instances, to automatically identify optimization opportunities, and
to automatically synthesize optimal protocols.

Biography

Ron van der Meyden is a Professor in the School of Computer Science
and Engineering at UNSW Sydney. His research
interests include the foundations of distributed and multi-agent
systems and computer security, and his contributions have included
work on deontic logic, deductive databases, foundations of public key
infrastructure, model checking and synthesis for epistemic logic, and
information flow security. He received the ACM Distinguished Scientist
Award in 2009.

Ron previously held positions at the University of Technology, Sydney,
the Weizmann Institute of Science, and NTT Basic Research
Laboratories, Tokyo, and has held visiting positions at NYU and
Stanford. He was a member of the teams that constructed successful
bids for and established the Cooperative Research Centre for Smart
Internet Technology and National ICT Australia (now part of
Data61). He served in 2001 as a research program leader in the
Cooperative Research Centre for Smart Internet Technology, before
establishing the Formal Methods program of National ICT Australia,
which he led from 2002 to 2006. Outcomes from this program include the
verification of the SeL4 micro-kernel, and Red Lizard Software, a
static analysis spinout which was acquired by Synopsys.