使用TLA+对CBC Casper共识算法进行形式化分析

作为Trail of Bits的暑期实习生，我使用PlusCal和TLA+形式化规范语言探索了以太坊的CBC Casper共识协议及其拜占庭容错特性。这项工作的灵感来源于Muneeb Ali、Jude Nelson和Aaron Blankstein在Medium.com上发表的《Peer Review: CBC Casper》一文，该文指出CBC Casper的活性属性比安全证明所建议的拜占庭容错阈值要求更严格。为了探索这一点，我在TLA+中指定了Casper the Friendly Binary共识协议。

正如预期的那样，如果拜占庭容错阈值不低于所有验证者总权重的三分之一，就无法确定最终性，这与Lamport等人关于拜占庭将军问题的原始论文一致。然而，只要满足这个条件，CBC Casper就能按预期运行。

背景介绍

CBC Casper（Correct By Construction）协议是一种权益证明（PoS）共识协议，设计用于未来的以太坊。然而，CBC Casper的当前状态尚未经过太多形式化分析，其规范不足对以太坊2.0的引入构成了挑战。

在分布式网络中，称为验证者的各个节点使用Minimal CBC Casper系列共识协议做出一致决策。该协议的五个参数是验证者的名称和权重、容错阈值、共识值和估计器。验证者根据其当前状态做出个体决策，该状态由接收到的消息定义，消息包含三个组成部分：

• 发送者：发送消息的验证者名称
• 估计值：共识值集合中的一个子集
• 证明：为达成估计而接收的一组消息（状态）

因此，消息的发送和接收可以定义为状态转换。

当验证者发送一对彼此不在对方证明中的消息时，就会发生Equivocation（双花）。未来状态是所有可到达的状态，其中Equivocation故障小于容错阈值。最终性由安全预言机定义，它检测某个属性是否在所有未来状态中都成立。

TLA+和PlusCal

TLA+是一种形式化规范语言，用状态和状态转换描述行为。规范和状态机模型可以用TLC模型检查器进行检查。TLC对定义的状态转换执行广度优先搜索，并检查需要满足的属性。

拜占庭将军问题

拜占庭将军问题是分布式系统中存在恶意个体时决策制定的一个类比。该问题指出，一个指挥官必须向n-1个副官发送命令，使得1）所有副官服从同一命令，2）如果指挥官忠诚，则每个忠诚的副官都服从该命令。问题的解决方案必须确保所有忠诚的将军就同一计划达成一致，并且少数叛徒不能导致将军们制定坏计划。

深入分析过程

首先，我在TLA+语言中指定了定义，并用集合和集合操作定义了状态和状态转换。图1显示了规范的一个片段。

图1：TLA+中的规范片段

我在PlusCal中指定了消息中继，它更类似于伪代码，可以自动转换为TLA+。

图2：在PlusCal中指定的CBC Casper消息中继

假设所有消息都能成功发送和接收，没有时间延迟。该规范不包括消息认证，因为假定验证者可以验证消息的真实性和来源。在此实现中，Equivocating验证者的行为是：它们获取所有接收消息的不同子集，使用这些子集获得估计值，并向不同的验证者发送不同的消息。

TLC模型检查器检查最终是否会找到一个 clique（团），其中所有非拜占庭节点可以相互看到对方在消息中同意某个估计值，并且不能相互看到对方不同意。当满足此条件时，就实现了最终性，模型检查器应终止而不报错，如图3所示。

图3：TLC模型检查结果

当无法达成最终性时，模型检查器将检测到时间属性被违反，如图4所示。

图4：TLC错误

时间属性检查是否存在一个验证者 clique，其总权重大于：

• Clique中的所有验证者满足以下条件：
  • 没有验证者是拜占庭故障。它们不发送Equivocating消息。
  • 所有验证者可以相互看到对方同意。每个验证者恰好有一条最新消息，并且它们具有相同的估计值。
  • 没有验证者可以相互看到对方不同意。一个验证者在另一个验证者的证明中有一条最新消息，但有一条新的最新消息，其估计值与另一个验证者的最新消息不同。

在实践中，无法达成最终性意味着区块链停止产生新区块，因为无法保证交易（即估计值）将来不会被逆转。

结论

我们发现，当容错阈值设置为大于所有验证者总权重的三分之一时，无法形成e-clique。这意味着当容错阈值小于总权重的三分之一时，可以达成最终性。这与“拜占庭将军问题”一致，该问题指出“当且仅当超过三分之二的将军忠诚时，问题才可解”。直观上，对于使用clique预言机的协议，较高的容错阈值会导致验证者太少而无法形成clique。

虽然CBC Casper规范提供了安全证明，但它没有解决活性属性。例如，CBC Casper区块链协议可能会遇到无法最终确定更多区块的问题。需要在指定活性方面进行进一步的工作，因为最终性是一个活性问题，并且对于转向PoS方法是必要的。我没有发现活性故障，但只测试了具有很少验证者的二进制共识。在更复杂的CBC Casper实例中可能存在活性故障。

关于形式化验证和TLA+的一些思考

开发抽象数学模型并系统地探索可能状态是检查算法正确性的一种有趣且重要的方式。然而，我遇到了以下挑战：

• TLA+语言实现细节的示例和形式化验证的最佳实践很少。因此，编写规范可能涉及大量试错。
• 当编译失败时，TLC模型检查器生成的错误消息没有帮助。错误消息模糊，无法精确定位错误发生的位置。此外，TLA+工具箱是一个Java应用程序，因此错误消息通常是Java异常。根据Java异常找出TLA+规范的问题很困难。
• 形式化验证方法的文档有限。在Google上搜索特定于TLA+的问题得到的结果非常少。截至[日期]，Stack Overflow上只有39个带有“TLA+”标签的问题。

致谢

今年夏天在Trail of Bits实习对我来说是一次美妙的经历。我学到了很多关于分布式系统和形式化验证的知识，并且非常喜欢这些主题。我很高兴能体验安全研究工作，并且有动力在大学里探索更多。

如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News