Byzantine consensus protocols aim at maintaining safety guarantees under any network synchrony model and at providing liveness in partially or fully synchronous networks. However, several Byzantine consensus protocols have been shown to violate liveness properties under certain scenarios. Existing testing methods for checking the liveness of consensus protocols check for time-bounded liveness violations, which generate a large number of false positives. In this work, for the first time, we check the liveness of Byzantine consensus protocols using the temperature and lasso detection methods, which require the definition of ad-hoc system state abstractions. We focus on the HotStuff protocol family that has been recently developed for blockchain consensus. In this family, the HotStuff protocol is both safe and live under the partial synchrony assumption, while the 2-Phase Hotstuff and Sync HotStuff protocols are known to violate liveness in subtle fault scenarios. We implemented our liveness checking methods on top of the Twins automated unit test generator to test the HotStuff protocol family. Our results indicate that our methods successfully detect all known liveness violations and produce fewer false positives than the traditional time-bounded liveness checks.

翻译：拜占庭共识协议旨在任何网络同步模型下保持安全性保证，并在部分同步或完全同步网络中提供活跃性。然而，已有研究表明，若干拜占庭共识协议在特定场景下会违反活跃性属性。现有的共识协议活跃性测试方法仅能检测时间有界内的活跃性违规，这会产生大量误报。本文首次采用温度和套索检测方法对拜占庭共识协议的活跃性进行检测，这需要定义特定于系统的状态抽象。我们聚焦于近期为区块链共识开发的HotStuff协议族。在该协议族中，HotStuff协议在部分同步假设下兼具安全性与活跃性，而2-Phase HotStuff和Sync HotStuff协议已知会在微妙故障场景下违反活跃性。我们在Twins自动化单元测试生成器基础上实现了活跃性检测方法，用于测试HotStuff协议族。结果表明，我们的方法成功检测到所有已知的活跃性违规，且相较于传统时间有界活跃性检测方法产生更少的误报。