他山之石 | 如何用 TLA+工具分析状态通道？

技术的突破是推动区块链行业前进的引擎，币安中国区块链研究院与链闻 ChainNews 同为密切关注区块链与密码学等领域技术发展前沿的组织，故而联合推出「他山之石」专栏，向中文世界读者介绍全球范围最值得关注的区块链技术进展，以及在金融等产业最新的应用分析与动态，以期为中国的区块链行业「攻玉」提供借鉴和思考。

本文解释了如何用 TLA+证明 force-move 协议为状态通道提供了担保，以确保你能提款。

原文标题：《 【他山之石】使用 TLA+分析状态通道 》
撰文：Tom Close，Magmo 团队负责人。本文基于 Andrew Stewart 的工作成果，在此感谢 Mike Kerzhner 和 George Knee 提出宝贵的意见和建议。

本文已取得作者授权，并由链闻和币安中国区块链研究院获得中文地区翻译首发权

目前我们在本系列的文章已经做了诸多与状态通道（state channel）相关的专题，其中一篇介绍了状态通道的底层担保机制：即在链是活动的且不存在监管的情况下，参与方能够在有限的时间内提款。我们引入了状体通道退出游戏（exit game）的一个玩具模型，并证明了该模型能够提供担保机制。

为了支持实际的应用，我们需要透过此玩具模型，转向更先进的状态通道系统，如此底层担保机制便能发挥作用吗？在本文中，我们阐述了如何使用 TLA+验证工具来测试我们的协议，以及如何修复该工具检测到的问题。

什么是 TLA+及使用 TLA+的原因

自发布 force-move 白皮书后，我们便一直在探寻证明该协议正确性的方法。由于状态通道涉及多个在链上和链外进行交互的参与方，所以很难照顾到所有的可能性。不过，我们肯定，这个协议没有问题。但是，我们经常会担心一些新出现的极端情况，直到确定没有问题，我们的疑虑才能打消。我们希望能找到一种方法，避免将来出现无法处理的情况，从而消除人们对该协议是否健全的担忧。

我们到底要证明什么？在此前关于通道融资的文章中，开头中提到了担保机制：即在链是活动的且不存在监管的情况下，参与方能够在有限的时间内提款。我们想证明，我们的状态通道系统也具备这样的特性。特别是，我们想证明，借助通道中交换的状态，无论其他参与方采取了什么行动，Alice 总是能在链上找到通向最终结果的一条路径。而且，这样的结果应该是「最新的」，因为其圈数（turn number）应至少与 Alice 当前的通道状态一样大。

出于其他的一些原因，我们首先研究了智能合约的形式验证，很快我们就意识到形式验证无法实现我们需要的担保程度。智能合约的形式验证能说明协议的实现没有问题，但是无法证明协议本身具备我们期望的性质。例如，如果你提交了一次 force-move，并签署上正确的状态，形式验证能证明注册了一次质询（challenge），但是用户如果想要在有限的时间内退出，无论其如何操作，形式验证无法证明用户所调用的一系列 force-move 操作。

在此背景下，Andrew 发现并意识到也许 TLA+正是我们所需要的。

TLA+是一种形式化规范语言，用于搭建算法或系统模型的工具，然后以编程方式验证此模型是否具备特定的属性。1999 年，Leslie Lamport 发布了这个工具，用来编写证明 Byzantine Paxos 正确性的形式证明。近期，AWS 的工程团队将其应用在了工业中，用于发现并修复 DynamoDB 中的并发性问题。

由于 TLA+的功能，有人将其描述成可充分测试的伪代码。正是这一点使其符合我们的需要。我们意识到，可以基于裁决人（adjudicator）以及在通道中与之交互的参与方，搭建一个模型。借助此模型及 TLA+，我们可以找出所有可允许操作的潜在序列，找出在哪些场景下，Alice 无法在指定的时段内提款。而且，如果我们能按照「对于长度为 n 的所有可能的操作序列，Alice 能在 m 步之内取出其资金，且 m<n」，通过穷举搜索证明一个声明，那么我们就知道 Alice 总是能在 m 步之内提款，从而也就证明了协议的安全性。

收获的见解

本节总结了 TLA+在从初版到最新版的连续三版协议下的应用情况。在该状态库中可找到模型的代码以及关于结果重建的说明。

在深入此模型之前，我们希望先呈现以下内容，因为据我们猜测，会有很多人对这些内容感兴趣。如果想了解全部的细节，建议先阅读最后的「模型」章节。

第一次尝试

我们首先尝试了 force-move 白皮书中定义的协议版本，这一版协议对 gas 进行了优化。此协议与《上手状态通道退出游戏》（Playing the State Channel Exit）一文中的玩具模型非常相似，区别在于，在此版本下，可以从质询中「恢复」并继续进行链下交互，而不必在发起首次质询后就结束。为了防止质询进入无限循环，裁决人需要跟踪其观察的最新受支持状态的轮号，并且只能允许可使此数值增大的质询。与裁决人进行交互的方法可总结如下：

这有一种发起质询的方法：forceMove(m,s*,p) 操作要求受支持状态 s*需要带有轮号 m，并且该操作必须由通道参与方 p 发起。假设 m 大于链上的轮号，则通道转换成质询状态 Chal(m,s,p)。

这里有三种响应 force-move 的方式。分别是：respond、refute 和 altRespond：

respond：是响应质询的「预期」方式

• 响应人提供下一状态，然后在链下继续进行交互。
• 链上的轮号计数器会计数，因为响应状态扩展了受支持的质询状态，故之后会再创建一个受支持的状态。

refute：是响应状态质询的一种方式

• 响应人提供由质询人签名的下一状态。
• 这么做可以代表质询人证明可证明的不良行为，所以，此时有机会在协议中构建 slashing
• 这种方式也非常高效，因为我们不需要检查任何状态转换
• 由于参与方只能看到一个状态，也就不需要告诉他们最新的受支持状态，所以链上的轮号计数器不会计数

altRespond：当参与方用相同的轮号签名了多个状态时，需要用到这种方式来说明情况

• 响应者提供一个会使轮号计数器+1 的新受支持状态。由于下一个受支持状态是可见的，所以链上的轮号计数器也会计数。
• 这就是响应人在说：「你已经质询了状态 s，但你之前给我发了一个状态 s'，所以我想从 s' 那里开始」

在任何情况下，由于性能优化的影响，必须提供质询状态 s 的一个副本，因为在优化版中，链上只储存了 s 的哈希值。接下来你会看到，这个看似微不足道的变化会对协议的健全性产生相当大的影响。

TLA+裁定

我们编写了这个模型的代码，接着在 TLA+中跑了一遍。TLA+并不喜欢这个模型，并且发现了以下失败场景：

1. 从 Open(n) 状态开始
   2.Alice 调用了 forceMove(n,s , Alice)
   3.Eve 利用 forceMove(n,s , Eve) 进行超前交易（front-run），将裁决人至于 Chal(n, s, Eve) 状态下。
   4.Alice 的 force-move 从第 2 步开始失败。
   5.Eve 调用 refute(n+k,s,s')，其中 k 大于 1，这样的话就轮到了 Eve，并且 s' 可以是任何轮号为 n+k 的有效状态。通道返回至 Open(n) 状态。
2. 转到第 1 步。

TLA+发现了一个无限循环，这个循环使 Eve 可以将资金无限期地锁定在通道中！当然，Eve 必须付款，但是，每次交易失败时，Alice 也在损失资金。而且损失率非常偏向 Eve：对应 Alice 的一笔交易，Eve 只需提交两笔交易（再加上一笔保险费，确保她每次都能超前交易）。无论如何，协议中都存在严重的漏洞。（实际上，我们事前已经对这个问题有所留意，但是我们没有想到 TLA+所发现的攻击方式会这么容易实现。）

不过，修复办法可不容易找到。造成这种循环的原因是 refute 不会使链上的轮号计数器计数，因为参与方不一定会看到新的受支持状态。验证链上的交易是确定存在新的受支持状态的唯一方法，但是 refute 的意义就在于取消可查验的不良质询，从而不耗费 gas 去运行链上的转换函数（transition function）。

我们想出的一种办法是在链上保存一份在当前的轮号计数器下已经成功调用了 force-move 的参与方名单，从而确保轮号计数器每次+1 时，参与方只能调用一次 force-move。由于对通道中参与方的数量没有限制，我们认为这样做太复杂了，同时浪费 gas。
最终，我们决定完全删除 refute 操作，以精简该协议。去掉对状态质询响应的优化也不是什么大问题，因此在此情况下，我们仍然可以选择引入 slashing，同时退还响应人的 gas 费用，这样似乎是一种更能激励正确行为的方式。

第二次尝试

在删除 refute 后，我们保留了以下操作：

TLA+裁定

我们在 TLA+中跑了一遍这个新模型。

这次的结果变好了：Alice 总是能使通道向前走。但是，其中仍存在造成损失的机会，Eve 可以拖延 Alice 一会儿，而具体拖多久则与当前的轮号成比例：

1. 从 Open(0) 状态开始
   2.Alice 调用 forceMove(n, s, Alice)
   3.Eve 利用 forceMove(0, s0, Eve) 进行超前交易（front-run），裁决人转换至 Chal(0, s0, Eve)。
   4.Alice 的 force-move 失败。
2. 然后，Eve 调用 respond(1, s0, s1)，将通道转换至 Open （1）。（如果 Eve 想要将 Alice 的损失最大化，那么她可以等到快超时再调用这个函数，因为她知道 Alice 可能不再持有此状态了）。
   6.Alice 调用 forceMove(n, s, Alice)
   7.Eve 利用 forceMove(1, s1, Eve) 进行超前交易
   8.……诸如此类

看来这里出现的问题至少与第 4 步存在一定的关联：forceMove 函数之所以失败，是因为在交易提交后，链的状态已经变化了。我们意识到，forceMove 应当覆盖之前的质询，并且使操作尽可能适用于更多的链状态似乎是不错的设计原则。

第三次尝试

在第三次尝试时，我们重写了 forceMove，使其能适用于质询状态，并且不再需要提供链上质询状态。在实现这一点的同时保证 gas 效率是个挺有趣的挑战，因为需要将大量的信息压缩至现有的 bytes32 通道存储区中。

此外，我们还考虑了另外的移动操作，也意识到了一些问题。首先，不应该将 altRespond 限制成仅使轮号+1，由于已经提供了完整的受支持状态，所以，无论增加了多少，都应使轮号计数器增至该状态的轮号。其次，这种情况不能仅发生在质询状态下，例如，当你需要长时间下线时，为了先发制人地提前排除大多数质询，根据开放状态（open state）增加轮号计数器也是非常实用的。

综上，altRespond 像是更基本的操作，因此我们决定将其重命名为 checkpoint （检查点）。然后，我们开始把 respond 视作更高效的 checkpoint 版本，用一个后续状态，优化了对 force-move 的响应。
我们最终得到了以下一系列操作：

TLA+裁定

成功！TLA+没发现任何问题，所以通过穷举搜索，我们知道此协议是可靠的。

不仅如此，假如 Alice 提交了 forceMove(n,s,Alice)，Alice 仅需一笔交易就能使通道向前走（或结束）。此交易失败的唯一可能是链上轮号计数器的次数 >n，在此情况下，通道已经前进了，并且 Alice 完成了交易。如果交易成功，则裁决人处于 Chal(n,s,Alice) 状态下，接下来的唯一可能是链上的轮号计数器计数或超时，从而结束通道。因此，仅提交一项交易，Alice 就实现了其目的。

这样可以保证条理有序，因为我们能严格限制 Alice 需要提交多少次交易才能退出通道：在最坏的情况下，Alice 需要调用 k 个事务，其中 k 是参与方的数量。第一个参与方 k-1 首先使通道向前走，直到轮到 Alice 为止，如上所述，最后一个用来 force-move 她自己，完成后，她便不再响应。

协议建模

在本节中，我们将更详细介绍如何设置 TLA+规范以上述内容。如果对本节不感兴趣，可以放心地跳过。

在深入研究我们的 TLA+建模决策之前，值得花一点时间来回顾我们的状态通道协议有哪些关键特性：force-move 协议围绕轮流制构建。在通道中交换的每个状态都有一个轮号，通过轮号可以确定哪个参与方在当时有权使通道向前走。例如，在有两个参与方的通道中，如果第一个参与方负责所有的偶数轮号，第二个参与方负责所有的奇数轮号。那么，一个状态必须由当时轮到的那个人签名，才能成为有效状态转换的一部分。

另外，引入受支持状态的概念也非常有用。在有 k 个参与方的通道中，受支持状态 s*是 k 个状态之间有效转换的序列，其最终状态为 s：s1->...-> sk = s （这是根据代码简化而来，可以达到我们当前的说明意图）。由于轮流属性，受支持状态总会包含各个参与方的签名。受支持状态类似于轮流制的完全签名状态，即表示所有参与方均参与了将通道推进至该状态。

下一步是检查我们要证明的内容，看看是否可以减少问题，以简化输入 TLA+的模型。

我们想证明，Alice 有一种策略，这种策略使她可以无视其他参与方所采取的操作，始终能在有限时间内得出链上最终敲定的最新结果。我们实际证明的是以下主张成立：

通道进度声明 ：如果 Alice 看到最新受支持状态的轮号是 n，那么她可以（a）获得一个轮号 > n 的受支持状态，或者（b）确保通道结束时状态的轮号 >= n。
为什么这就够了？假设在轮号是 n + m 时会再次轮到 Alice。如果 Alice 不用这个轮号签名任何状态，那么没有受支持的状态会带有此轮号或更高的轮号。因此，通过应用 m 次通道进度声明，唯一可能的结果是该通道最终结束时状态的轮号 >= n。

我们还需要指定该声明成立的条件。我们的模型捕捉了以下场景：

• Alice 是状态通道中一名诚实的参与方，持有受支持的状态，状态的轮号是 n。
• Alice 的目标是（a）获得一个轮号大于 n 的受支持状态，或（b）在轮号大于等于 n 的状态下关闭通道
• Alice 只储存了最后一轮的状态，因此只能访问最新受支持的状态。（这很重要，因为这意味着对于诚实的参与方而言，存储需求会根据开放通道（open channel）的数量而非状态总数来扩展。）
• Alice 总是能在质询期内将交易打包，但是无法进行超前交易，也无法阻止别人进行超前交易。
• 仅在（a）轮到她的时候，Alice 才能给状态签名，并且（b）表示从她所持有的受支持状态开始的有效转换。
• Eve 是她的对手，控制着通道中其他的参与方。
• Eve 储存了在通道中交易的所有历史状态。
• Eve 愿意给过去或未来的任何状态签名，但不表示从她所持有的受支持状态开始的有效转换。她无法签名的状态是那些轮到 Alice 签名的状态，其轮号 > n，因为这些状态只有 Alice 可以签名，但她还没签。
• Eve 可以任意地在 Alice 之前进行超前交易，但无法阻止 Alice 的交易在质询期内被打包。

如何用 TLA+给此场景建模？如果你够勇敢，可以去代码中自己找，也可以看我们在这里的总结概括。

首先要了解的是，TLA+规范涉及到了多个过程，这些过程创建了修改共享状态的操作。在模拟系统时，TLA+会搜索通过插入过程操作创建的所有潜在序列，在达到共享状态上的某些条件时，则会停止各个序列。

在我们的案例中，Alice 和 Eva 是独立的过程，裁决人构成共享状态的一部分。为了捕获到超前交易行为，我们需要引入一个额外的过程和状态——交易处理器（transaction processor）和交易池（transaction pool）。当 Eve 流程直接修改裁决人状态时，Alice 只能将交易放入交易池中，然后交易池会把此交易交给裁决人。

TLA+的概念是「公平过程」（fair process），即其行动不会受到无限阻碍的过程。这正是我们建模「Eve 可以任意地在 Alice 之前进行超前交易，但 Alice 最终会得到一笔交易」的行为所需要的工具。我们没有明确地对超时本身进行建模，因为我们知道，只要 Alice 或 Eve 持有能避免超时的状态，她们一定会避免超时。因此，发生超时的情况恰好是无法采取其他行动的情况，而 TLA +会自动阻止这种情况的发生。

就成功标准而言，有必要把声明从「Alice 可在有限的时间内成功」改成「Alice 可在 N 步内成功」，其中 N 由我们决定。在这样的修改后，我们可以确保 TLA+是在有限的、可管理的状态空间内进行搜索。

另外，我们还选出了一对参与方来进行模拟。具体地说，我们证明了「在任何由 2 个参与方组成的通道内，Alice 可以在 5 步内实现其目标」。当然，尽管还不足以证明所有通道的声明，但是，确实为由少量参与方组成的通道提供了坚实的保障，这正是我们在实际应用中所关心的。我们也越来越相信，这种方法适用于任意数量的参与方，即便有额外的参与方，也不会有任何变化——在设置模型时，我们就有这种感觉。

总结

在本文中，我们解释了如何用 TLA+证明 force-move 协议为状态通道提供了担保，以确保你能提款。

下周，随着 Web3Torrent 项目的发布，我们将从理论转向实践。Web3Torrent 改善了 Webtorrent 的点对点文件共享，在状态通道上构建了点对点微支付。我们希望它能证明当今状态通道的可能性，启发更多人在其机制设计中使用微支付 / 状态通道。敬请期待！

来源链接： blog.statechannels.org