使用TLA+对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+规范问题很困难
- 形式化验证方法的文档有限，搜索TLA+特定问题得到的结果很少
致谢
在Trail of Bits的暑期实习是一次宝贵经历，学习了分布式系统和形式化验证知识，非常享受这些主题。很高兴能体验安全研究工作，进入大学后更有动力继续探索。