Formally verified Byzantine agreement in presence of link faults

This paper shows that deterministic consensus in synchronous distributed systems with link faults is possible, despite the impossibility result of Gray (1978). Instead of using randomization, we overcome this impossibility by moderately restricting the inconsistency that link faults may cause system-wide. Relying upon a novel hybrid fault model that provides different classes of faults for both nodes and links, we provide a formally verified proof that the m+1-round Byzantine agreement algorithm OMH (Lincoln and Rushby (1993)) requires n > 2f_l^s + f_l^r + f_l^ra + 2(f_a + f_s) + f_o + f_m + m nodes for transparently masking at most f_l^s broadcast and f_l^r receive link faults (including at most f_l^ra arbitrary ones) per node in each round, in addition to at most f_a, f_s, f_o, f_m arbitrary, symmetric, omission, and manifest node faults, provided that m ≥ f_a + f_o + 1. Our approach to modeling link faults is justified by a number of theoretical results, which include tight lower bounds for the required number of nodes and an analysis of the assumption coverage in systems where links fail independently with some probability p.