![]() |
![]() |
University of Birmingham > Talks@bham > Computer Security Seminars > Verification of Byzantine Fault Tolerant Systems
Verification of Byzantine Fault Tolerant SystemsAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsTheoretical Physics Journal Club Type the title of a new list here EPS - College Research and KT Support ActivitiesOther talksThe tragic destiny of Mileva Marić Einstein TBA An introduction to τ-exceptional sequences Wave turbulence in the Schrödinger-Helmholtz equation Life : it’s out there, but what and why ? Waveform modelling and the importance of multipole asymmetry in Gravitational Wave astronomy |