技术的突破是推动区块链行业前进的引擎，币安中国区块链研究院与链闻ChainNews同为密切关注区块链与密码学等领域技术发展前沿的组织，故而联合推出「他山之石」专栏，向中文世界读者介绍全球范围最值得关注的区块链技术进展，以及在金融等产业最新的应用分析与动态，以期为中国的区块链行业「攻玉」提供借鉴和思考。
本文解释了如何用TLA证明force-move协议为状态通道提供了担保，以确保你能提款。
原文标题：《使用TLA分析状态通道》撰文：TomClose，Magmo团队负责人。本文基于AndrewStewart的工作成果，在此感谢MikeKerzhner和GeorgeKnee提出宝贵的意见和建议。
本文已取得作者授权，并由链闻和币安中国区块链研究院获得中文地区翻译首发权
目前我们在本系列的文章已经做了诸多与状态通道相关的专题，其中一篇介绍了状态通道的底层担保机制：即在链是活动的且不存在监管的情况下，参与方能够在有限的时间内提款。我们引入了状体通道退出游戏的一个玩具模型，并证明了该模型能够提供担保机制。
为了支持实际的应用，我们需要透过此玩具模型，转向更先进的状态通道系统，如此底层担保机制便能发挥作用吗？在本文中，我们阐述了如何使用TLA验证工具来测试我们的协议，以及如何修复该工具检测到的问题。
什么是TLA及使用TLA的原因
自发布force-move白皮书后，我们便一直在探寻证明该协议正确性的方法。由于状态通道涉及多个在链上和链外进行交互的参与方，所以很难照顾到所有的可能性。不过，我们肯定，这个协议没有问题。但是，我们经常会担心一些新出现的极端情况，直到确定没有问题，我们的疑虑才能打消。我们希望能找到一种方法，避免将来出现无法处理的情况，从而消除人们对该协议是否健全的担忧。
我们到底要证明什么？在此前关于通道融资的文章中，开头中提到了担保机制：即在链是活动的且不存在监管的情况下，参与方能够在有限的时间内提款。我们想证明，我们的状态通道系统也具备这样的特性。特别是，我们想证明，借助通道中交换的状态，无论其他参与方采取了什么行动，Alice总是能在链上找到通向最终结果的一条路径。而且，这样的结果应该是「最新的」，因为其圈数应至少与Alice当前的通道状态一样大。
数据：比特币今日凌晨某区块出块时间达1小时40分钟:5月19日消息，Dune数据显示，比特币在北京时间5月19日凌晨01:18区块高度790340处的出块时间达1小时40分钟35秒，为今年出块最慢的比特币区块，且是过去一年中出块第三慢的比特币区块。此外，Btc.com数据显示，区块高度790340处的交易数达2141，交易总额达11659.23枚BTC。[2023/5/19 15:13:09]
出于其他的一些原因，我们首先研究了智能合约的形式验证，很快我们就意识到形式验证无法实现我们需要的担保程度。智能合约的形式验证能说明协议的实现没有问题，但是无法证明协议本身具备我们期望的性质。例如，如果你提交了一次force-move，并签署上正确的状态，形式验证能证明注册了一次质询，但是用户如果想要在有限的时间内退出，无论其如何操作，形式验证无法证明用户所调用的一系列force-move操作。
在此背景下，Andrew发现并意识到也许TLA正是我们所需要的。
TLA是一种形式化规范语言，用于搭建算法或系统模型的工具，然后以编程方式验证此模型是否具备特定的属性。1999年，LeslieLamport发布了这个工具，用来编写证明ByzantinePaxos正确性的形式证明。近期，AWS的工程团队将其应用在了工业中，用于发现并修复DynamoDB中的并发性问题。
由于TLA的功能，有人将其描述成可充分测试的伪代码。正是这一点使其符合我们的需要。我们意识到，可以基于裁决人以及在通道中与之交互的参与方，搭建一个模型。借助此模型及TLA，我们可以找出所有可允许操作的潜在序列，找出在哪些场景下，Alice无法在指定的时段内提款。而且，如果我们能按照「对于长度为n的所有可能的操作序列，Alice能在m步之内取出其资金，且m收获的见解
本节总结了TLA在从初版到最新版的连续三版协议下的应用情况。在该状态库中可找到模型的代码以及关于结果重建的说明。
在深入此模型之前，我们希望先呈现以下内容，因为据我们猜测，会有很多人对这些内容感兴趣。如果想了解全部的细节，建议先阅读最后的「模型」章节。
第一次尝试
我们首先尝试了force-move白皮书中定义的协议版本，这一版协议对gas进行了优化。此协议与《上手状态通道退出游戏》一文中的玩具模型非常相似，区别在于，在此版本下，可以从质询中「恢复」并继续进行链下交互，而不必在发起首次质询后就结束。为了防止质询进入无限循环，裁决人需要跟踪其观察的最新受支持状态的轮号，并且只能允许可使此数值增大的质询。与裁决人进行交互的方法可总结如下：
这有一种发起质询的方法：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并不喜欢这个模型，并且发现了以下失败场景：
从Open(n)状态开始2.Alice调用了forceMove(n,s,Alice)3.Eve利用forceMove(n,s,Eve)进行超前交易，将裁决人至于Chal(n,s,Eve)状态下。4.Alice的force-move从第2步开始失败。5.Eve调用refute(nk,s,s')，其中k大于1，这样的话就轮到了Eve，并且s'可以是任何轮号为nk的有效状态。通道返回至Open(n)状态。转到第1步。TLA发现了一个无限循环，这个循环使Eve可以将资金无限期地锁定在通道中！当然，Eve必须付款，但是，每次交易失败时，Alice也在损失资金。而且损失率非常偏向Eve：对应Alice的一笔交易，Eve只需提交两笔交易。无论如何，协议中都存在严重的漏洞。
不过，修复办法可不容易找到。造成这种循环的原因是refute不会使链上的轮号计数器计数，因为参与方不一定会看到新的受支持状态。验证链上的交易是确定存在新的受支持状态的唯一方法，但是refute的意义就在于取消可查验的不良质询，从而不耗费gas去运行链上的转换函数。
我们想出的一种办法是在链上保存一份在当前的轮号计数器下已经成功调用了force-move的参与方名单，从而确保轮号计数器每次1时，参与方只能调用一次force-move。由于对通道中参与方的数量没有限制，我们认为这样做太复杂了，同时浪费gas。最终，我们决定完全删除refute操作，以精简该协议。去掉对状态质询响应的优化也不是什么大问题，因此在此情况下，我们仍然可以选择引入slashing，同时退还响应人的gas费用，这样似乎是一种更能激励正确行为的方式。
第二次尝试
在删除refute后，我们保留了以下操作：
TLA裁定
我们在TLA中跑了一遍这个新模型。
这次的结果变好了：Alice总是能使通道向前走。但是，其中仍存在造成损失的机会，Eve可以拖延Alice一会儿，而具体拖多久则与当前的轮号成比例：
从Open(0)状态开始2.Alice调用forceMove(n,s,Alice)3.Eve利用forceMove(0,s0,Eve)进行超前交易，裁决人转换至Chal(0,s0,Eve)。4.Alice的force-move失败。然后，Eve调用respond(1,s0,s1)，将通道转换至Open。。6.Alice调用forceMove(n,s,Alice)7.Eve利用forceMove(1,s1,Eve)进行超前交易8.……诸如此类看来这里出现的问题至少与第4步存在一定的关联：forceMove函数之所以失败，是因为在交易提交后，链的状态已经变化了。我们意识到，forceMove应当覆盖之前的质询，并且使操作尽可能适用于更多的链状态似乎是不错的设计原则。
第三次尝试
在第三次尝试时，我们重写了forceMove，使其能适用于质询状态，并且不再需要提供链上质询状态。在实现这一点的同时保证gas效率是个挺有趣的挑战，因为需要将大量的信息压缩至现有的bytes32通道存储区中。
此外，我们还考虑了另外的移动操作，也意识到了一些问题。首先，不应该将altRespond限制成仅使轮号1，由于已经提供了完整的受支持状态，所以，无论增加了多少，都应使轮号计数器增至该状态的轮号。其次，这种情况不能仅发生在质询状态下，例如，当你需要长时间下线时，为了先发制人地提前排除大多数质询，根据开放状态增加轮号计数器也是非常实用的。
综上，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，那么她可以获得一个轮号>n的受支持状态，或者确保通道结束时状态的轮号>=n。为什么这就够了？假设在轮号是nm时会再次轮到Alice。如果Alice不用这个轮号签名任何状态，那么没有受支持的状态会带有此轮号或更高的轮号。因此，通过应用m次通道进度声明，唯一可能的结果是该通道最终结束时状态的轮号>=n。
我们还需要指定该声明成立的条件。我们的模型捕捉了以下场景：
Alice是状态通道中一名诚实的参与方，持有受支持的状态，状态的轮号是n。Alice的目标是获得一个轮号大于n的受支持状态，或在轮号大于等于n的状态下关闭通道Alice只储存了最后一轮的状态，因此只能访问最新受支持的状态。的数量而非状态总数来扩展。）Alice总是能在质询期内将交易打包，但是无法进行超前交易，也无法阻止别人进行超前交易。仅在轮到她的时候，Alice才能给状态签名，并且表示从她所持有的受支持状态开始的有效转换。Eve是她的对手，控制着通道中其他的参与方。Eve储存了在通道中交易的所有历史状态。Eve愿意给过去或未来的任何状态签名，但不表示从她所持有的受支持状态开始的有效转换。她无法签名的状态是那些轮到Alice签名的状态，其轮号>n，因为这些状态只有Alice可以签名，但她还没签。Eve可以任意地在Alice之前进行超前交易，但无法阻止Alice的交易在质询期内被打包。
如何用TLA给此场景建模？如果你够勇敢，可以去代码中自己找，也可以看我们在这里的总结概括。
首先要了解的是，TLA规范涉及到了多个过程，这些过程创建了修改共享状态的操作。在模拟系统时，TLA会搜索通过插入过程操作创建的所有潜在序列，在达到共享状态上的某些条件时，则会停止各个序列。
在我们的案例中，Alice和Eva是独立的过程，裁决人构成共享状态的一部分。为了捕获到超前交易行为，我们需要引入一个额外的过程和状态——交易处理器和交易池。当Eve流程直接修改裁决人状态时，Alice只能将交易放入交易池中，然后交易池会把此交易交给裁决人。
TLA的概念是「公平过程」，即其行动不会受到无限阻碍的过程。这正是我们建模「Eve可以任意地在Alice之前进行超前交易，但Alice最终会得到一笔交易」的行为所需要的工具。我们没有明确地对超时本身进行建模，因为我们知道，只要Alice或Eve持有能避免超时的状态，她们一定会避免超时。因此，发生超时的情况恰好是无法采取其他行动的情况，而TLA会自动阻止这种情况的发生。
就成功标准而言，有必要把声明从「Alice可在有限的时间内成功」改成「Alice可在N步内成功」，其中N由我们决定。在这样的修改后，我们可以确保TLA是在有限的、可管理的状态空间内进行搜索。
另外，我们还选出了一对参与方来进行模拟。具体地说，我们证明了「在任何由2个参与方组成的通道内，Alice可以在5步内实现其目标」。当然，尽管还不足以证明所有通道的声明，但是，确实为由少量参与方组成的通道提供了坚实的保障，这正是我们在实际应用中所关心的。我们也越来越相信，这种方法适用于任意数量的参与方，即便有额外的参与方，也不会有任何变化——在设置模型时，我们就有这种感觉。
总结
在本文中，我们解释了如何用TLA证明force-move协议为状态通道提供了担保，以确保你能提款。
下周，随着Web3Torrent项目的发布，我们将从理论转向实践。Web3Torrent改善了Webtorrent的点对点文件共享，在状态通道上构建了点对点微支付。我们希望它能证明当今状态通道的可能性，启发更多人在其机制设计中使用微支付/状态通道。敬请期待！
来源链接：blog.statechannels.org
免责声明：作为区块链信息平台，本站所发布文章仅代表作者个人观点，与链闻ChainNews立场无关。文章内的信息、意见等均仅供参考，并非作为或被视为实际投资建议。
币安
币安
币安Binance区块链数字资产交易平台，引领币币交易创新模式，为用户提供更加安全、便捷的数字货币兑换服务，聚合全球优质数字货币，致力于打造世界级的区块链资产交易平台。提供比特币、以太坊、莱特币、币安币等主流加密数字货币交易。公司几乎所有的资产，包括对于交易收取的费用及拿到的融资，都以加密数字货币形式保存。币安BinanceBNBBinanceChainBinanceLabsBinanceLabs币安慈善币安慈善基金会币安孵化器BinanceDEX币安宝币安研报币安研究院BinanceResearch币安美国BinanceFuturesBinanceLaunchpad币安云BinanceCloudBinanceCardBinance.US币安Launchpad币安LaunchpoolBinancePay查看更多
郑重声明： 本文版权归原作者所有， 转载文章仅为传播更多信息之目的， 如作者信息标记有误， 请第一时间联系我们修改或删除， 多谢。