Number SRI-CSL-93-2.
Computer Science Laboratory, SRI International.
March, 1993.
Consistent distribution of single-source data to replicated computing channels is a
fundamental problem in fault-tolerant system design. The ``Oral Messages'' (OM)
algorithm of Lamport, Shostak, and Pease solves this problem of Interactive Consistency
(also known as Source Congruence or Byzantine Agreement) in the presence of m arbitrary
(i.e., Byzantine) Faults, using m+1 rounds of message exchange and n > 3m channels.
A problem with OM and similar algorithms is that all faults are assumed to exhibit
worst-case (i.e., arbitrary) behavior, so that the algorithm can tolerate no more ``simple''
faults than truly Byzantine ones. To overcome this deficiency, Thambidurai and Park
introduced a ``hybrid'' fault model that distinguished three fault modes: asymmetric
(Byzantine), symmetric, and benign; they also exhibited, along with an informal ``proof of
correctness,'' a modified version of OM that withstands a asymmetric, s symmetric, and b
benign faults simultaneously, using m+1 rounds, provided n> 2a + 2s + b + m, and m >= a.
Unfortunately, this algorithm is flawed; it fails, for example, in the case n=5, m=1 when the
transmitter has a benign fault and one of the receivers is Byzantine. We detected this flaw
while undertaking a formal verification of the algorithm using our PVS mechanical
verification system. Repairing this algorithm is not easy. We developed an incorrect version
ourselves, and even ``proved'' it correct using ordinary, informal mathematics.
The discipline of mechanically checked formal verification eventually enabled us to develop a
correct algorithm for Interactive Consistency under the hybrid fault model. We present this
algorithm, discuss its subtle points, and describe its formal specification and verification.
We argue that formal verification systems such as PVS are now sufficiently effective that
their application to fault-tolerance algorithms should be considered routine.
@techreport{csl-93-2,
AUTHOR = {Patrick Lincoln and John Rushby},
TITLE = {{A} Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model},
INSTITUTION = {Computer Science Laboratory, {SRI} International},
YEAR = {1993},
NUMBER = {{SRI-CSL-93-2}},
MONTH = {mar},
NOTE = {Also available as {NASA} Contractor Report 4527, July 1993},
URL = {http://www.csl.sri.com/papers/csl-93-2/}
}
R&D Divisions