Verification of Byzantine Fault Tolerant Systems

Add to your list(s) Download to your calendar using vCal

• Vincent Rahli (University of Birmingham)
• Thursday 06 February 2020, 11:00-12:00
• Computer Science, The Sloman Lounge (UG).

If you have a question about this talk, please contact Isra Ahmed.

Embracing the fact that programs will always have unforseen bugs and vulnerabilities, Byzantine Fault Tolerant State-Machine Replication (BFT-SMR) is a generic technique to turn a service into one that can tolerate arbitrary faults. It works by replicating (and diversifying) the service across several machines, while making sure that the replicas behave as a single entity. Even if the replicated service has defects, for this technique to be of any use, the replication protocol itself at least needs to be correct. Unfortunately, such replication protocols tend to be quite complex, and are still hard to get right, as they typically rely on complex exchanges of messages. Another drawback of such protocols is alo that they are expansive (a total of 3f+1 replicas is typically required to tolerate at most f faulty replicas). In this talk, I will briefly explain how BFT -SMR works and I will present a few landmark protocols. I will then describe a technique (called hybridization), which is used to reduce the cost of BFT -SMR. I will finally describe two tools that we have built within the Coq theorem prover, to help verify implementations of such BFT -SMR systems. This is joint work with Ivana Vukotic.

This talk is part of the Computer Security Seminars series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, The Sloman Lounge (UG)
• Computer Security Seminars
• computer sience

Note that ex-directory lists are not shown.