University of Birmingham > Talks@bham > Computer Security Seminars > Verification of Byzantine Fault Tolerant Systems

Verification of Byzantine Fault Tolerant Systems

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.