SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

A Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model (IEEE)
 by Dr. Patrick Lincoln & Dr. John Rushby.

Number SRI-CSL-93-2.
Computer Science Laboratory, SRI International.
March, 1993.

Also available as NASA Contractor Report 4527, July 1993


Abstract

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.

BibTEX Entry
@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/}
}
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy