用于测试共识实现的领域特定语言
摘要：大规模、容错、分布式系统是许多关键软件服务的支撑。由于它们必须在可能具有任意通信延迟和故障的对抗环境中正确执行，所以底层算法非常复杂。特别是，实现一致性和数据保留依赖于复杂的一致性（状态机复制）协议。由于在生产过程中可能出现大量异常情况，确保此类协议实现的可靠性仍然是一个重大挑战。我们提出了一种名为Netrix的方法和工具来测试这种实现，旨在利用程序员的知识来提高覆盖率，实现强大的漏洞再现，并可在不同版本的实现中进行回归测试。作为评估，我们将我们的工具应用于一种流行的权益证明区块链协议Tendermint，该协议依赖于拜占庭一致性算法、良性一致性算法Raft和BFT-Smart。我们能够发现Tendermint实现与协议规范之间的4个差异，并在更新的实现上检查它们的缺失。此外，我们能够再现Raft中已知的4个漏洞。
作者：Cezara Dragoi, Constantin Enea, Srinidhi Nagendra, Mandayam Srivas
论文ID：2303.05893
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-25