The formal verification of an algorithm for interactive consistency under a hybrid fault model

Abstract

Modern verification systems such as PVS are now reaching the stage of development where the formal verification of critical algorithms is feasible with reasonable effort. This paper describes one such verification in the field of fault tolerance. The distribution of single source data to replicated computing channels (Interactive Consistency or Byzantine Agreement) is a central problem in this field. The classic Oral Messages (OM) algorithm solves this problem under the assumption that all channels are either nonfaulty or arbitrary (Byzantine) faulty. Thambidurai and Park have introduced a "hybrid" fault model that distinguishes additional fault modes, along with a modified version of OM. They gave an informal proof that their algorithm withstands the same number of arbitrary faults, but more "nonmalicious" faults than OM. We detected a flaw in this algorithm while undertaking its formal verification using PVS, The discipline of mechanically-checked formal verification helped us to develop a corrected version of the algorithm. Here we describe the formal specification and verification of this new algorithm. We argue that formal verification systems such as PVS are now sufficiently effective that their application to critical fault-tolerance algorithms should be considered routine.