Reference : Formal Framework for Verifying Implementations of Byzantine Fault-Tolerant Protocols ...
Dissertations and theses : Doctoral thesis
Engineering, computing & technology : Computer science
Security, Reliability and Trust
Formal Framework for Verifying Implementations of Byzantine Fault-Tolerant Protocols Under Various Models
Vukotic, Ivana mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
University of Luxembourg, ​Esch sur Alzette, ​​Luxembourg
143 + 52
Esteves-Verissimo, Paulo mailto
Ryan, Peter Y A mailto
Volp, Marcus mailto
Merz, Stephan mailto
Rushby, John mailto
Rahli, Vincent mailto
Correia, Miguel mailto
[en] Fault-tolerance ; Byzantine fault ; SM ; PBFT ; MinBFT ; Formal verification ; Compositional reasoning ; Coq ; Knowledge calculus ; Monad ; Step-indexing ; Hybrid protocols
[en] The complexity of critical systems our life depends on (such as water supplies, power grids, blockchain systems, etc.) is constantly increasing. Although many different techniques can be used for proving correctness of these systems errors still exist, because these techniques are either not complete or can only be applied to some parts of these systems. This is why fault and intrusion tolerance (FIT) techniques, such as those along the well-known Byzantine Fault-Tolerance paradigm (BFT), should be used.

BFT is a general FIT technique of the active replication class, which enables seamless correct functioning of a system, even when some parts of that system are not working correctly or are compromised by successful attacks. Although powerful, since it systematically masks any errors, standard (i.e., ``homogeneous'') BFT protocols are expensive both in terms of the messages exchanged, the required number of replicas, and the additional burden of ensuring them to be diverse enough to enforce failure independence. For example, standard BFT protocols usually require 3f+1 replicas to tolerate up to f faults.

In contrast to these standard protocols based on homogeneous system models, the so-called hybrid BFT protocols are based on architectural hybridization: well-defined and self-contained subsystems of the architecture (hybrids) follow system model and fault assumptions differentiated from the rest of the architecture (the normal part). This way, they can host one or more components trusted to provide, in a trustworthy way, stronger properties than would be possible in the normal part. For example, it is typical that whilst the normal part is asynchronous and suffers arbitrary faults, the hybrids are synchronous and fail-silent. Under these favorable conditions, they can reliably provide simple but effective services such as perfect failure detection, counters, ordering, signatures, voting, global timestamping, random numbers, etc. Thanks to the systematic assistance of these trusted-trustworthy components in protocol execution, hybrid BFT protocols dramatically reduce the cost of BFT. For example, hybrid BFT protocols require 2f+1 replicas instead of 3f +1 to tolerate up to f faults.

Although hybrid BFT protocols significantly decrease message/time/space complexity vs. homogeneous ones, they also increase structural complexity and as such the probability of finding errors in these protocols increases. One other fundamental correctness issue not formally addressed previously, is ensuring that safety and liveness properties of trusted-trustworthy component services, besides being valid inside the hybrid subsystems, are made available, or lifted, to user components at the normal asynchronous and arbitrary-on-failure distributed system level.

This thesis presents a theorem-prover based, general, reusable and extensible framework for implementing and proving correctness of synchronous and asynchronous homogeneous FIT protocols, as well as hybrid ones. Our framework comes with: (1) a logic to reason about homogeneous/hybrid fault-models; (2) a language to implement systems as collections of interacting homogeneous/hybrid components; and (3) a knowledge theory to reason about crash/Byzantine homogeneous and hybrid systems at a high-level of abstraction, thereby allowing reusing proofs, and capturing the high-level logic of distributed systems. In addition, our framework supports the lifting of properties of trusted-trustworthy components, first to the level of the local subsystem the trusted component belongs to, and then to the level of the distributed system. As case studies and proofs-of-concept of our findings, we verified seminal protocols from each of the relevant categories: the asynchronous PBFT protocol, two variants of the synchronous SM protocol, as well as two versions of hybrid MinBFT protocol.
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Critical and Extreme Security and Dependability Research Group (CritiX)
Researchers ; Professionals ; Students ; General public
FnR ; FNR8149128 > Paulo Esteves-Veríssimo > IISD > Strategic RTnD Program on Information Infrastructure Security and Dependability > 01/01/2015 > 31/12/2019 > 2014

File(s) associated to this reference

Additional material(s):

File Commentary Size Access
Open access
thesis+code.zip5.26 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.