A livelock bug in the presence of byzantine validator

[sifmelcara]

Hello, our team are re-implementing the elegant tendermint byzantine consensus algorithm described in the wiki.

However, we found a liveness bug can happen when malicious byzantine validators are participating (if they have a carefully planned strategy). Also we found this bug may have already been pointed out in Christian Cachin (@cca88) and Marko Vukolić's paper, Blockchain Consensus Protocols in the Wild page 11:

Tendermint as originally described by Buchman [13] suffers from a livelock bug, pertaining to locking
and unlocking votes by validators in the protocol. However, the protocol contains additional mechanisms not described in the cited report that prevent the livelock from occurring [14].

The reference number 14 is "E. Buchman and J. Kwon. Private discussion, 2017.".
Since tendermint is the pioneer of BFT consensus algorithm in the age of blockchain, and also powers critical services like Cosmos, I think it would be great if people can learn more about the detail of consensus mechanism. @ebuchman @jaekwon would you mind to share the additional mechanisms mentioned by @cca88's paper?

Thank you for all that you've done to this awesome project!

[ebuchman]

Thanks for opening this and for your support for the project! What language are you implementing Tendermint in ? Is the code open source?

Indeed there was a live lock bug in my thesis that is not in the code itself. See the consensus/reactor.go file for the gossiping mechanism we use.

We are working on more comprehensive and superior documentation and specification for the algorithm and the implementation. You can see a start in https://github.com/tendermint/tendermint/tree/develop/docs/specification/new-spec

We will be publishing a full formal specification and safety and liveness proofs for the Tendermint consensus algorithm very soon - stay tuned!

[sifmelcara]

Thanks for the reply. So basically because of gossiping, eventually it is unlikely that only some correct processes receive a specific message. Do I understand right?
In fact we are making a consensus algorithm design framework which algorithm designers can specify their algorithm in. Then the properties of consensus are checked using model checking techniques (it also generates an implementation). By doing this, we can assure the algorithm remain correct no matter how do those byzantine participants attack.
However, when we encode the Tendermint's algorithm in the framework, a counter example violates liveness is emitted, so we doubts if we were missing assumptions or implementation details of tendermint.
The prototype is written in Haskell and uses zeromq to exchange messages. It is still in early stage and I think it will definitely be open sourced if we can overcome the challenges (to make the framework actually useful to evaluate consensus algorithms).

[milosevic]

Yes, you are right. If a correct process receives a message, it will gossip it to other processes, so eventually (with high probability) all correct processes will get it.
It is very interesting what you are working on. We would be happy to understand more details. How we can reach you guys?

[sifmelcara]

Sorry for the late reply. Please contact me via mingcl.tw@gmail. I'm looking forward for your comments, thanks!
(Closing this issue since the mechanism have been clarified)