3
作者: Internet Computer / Dfinity
编译: ChainCatcher
Temporal Logic of Actions (TLA+) 是一个通用工具包，可以详尽地测试软件设计，也适用于 ckBTC 智能合约。告别重入错误，迎接更安全的 BTC <> ICP 传输。
由 Ognjen Maric 撰写
2016 年 6 月，兴奋情绪高涨。 \"The DAO\"，建立在以太坊区块链之上，即将成为全球首个全数字化、去中心化的投资基金。但在几周内，在攻击者从中窃取了价值 5000 万美元的以太币之后，它反而成为了 DeFi 黑客攻击的典型代表。
为了破解 The DAO，攻击者利用了所谓的重入漏洞，这是一种并发漏洞，其中调用特定智能合约的一个方法，而另一个方法仍在执行。而 The DAO 只是智能合约长期发展过程中的第一个，受到此类错误的困扰。突出的继任者包括 Uniswap/Lendf.Me，在 2020 年被盗 2500 万美元，CREAM 在 2021 年被盗 1800 万美元，Fei 在 2022 年被盗 8000 万美元。这些错误持续存在的原因是它们可能涉及分散在整个系统中的意外代码交互智能合约，有时甚至完全在不同的智能合约中。此类代码交互的数量可能非常庞大，因此人类很难检测并剔除不需要的代码。此外，这些交互通常很难自动和系统地测试。
TLA+：Exterminator 输入时间逻辑操作 (TLA+)，一种用于指定和验证复杂系统的语言。 TLA+ 不仅可以发现错误，还可以验证它们是否存在。你问这怎么可能？ TLA+ 带有一组工具，用于以所谓的模型检查的形式进行轻量级形式验证。通过模型检查，它详尽地探索了代码模型的所有可能并发交互——正是难以测试的领域——并发现了错误。想象一个灭虫者，他照亮每个角落和缝隙，暴露并消灭隐藏在那些经常被遗漏或忽视的黑暗角落里的不需要的害虫。重要的是，在构建代码模型后，模型检查几乎无需进一步的人工输入即可运行，因此具有很高的成本效益。用一些虚构的数字来说明：如果行业标准实践（如测试和安全审查）消除了 80% 的错误，而\"重量级\"形式验证消除了 99%，而使用 TLA+ 则可以消除 90% 的一小部分重量级验证的努力。
TLA+ 和互联网计算机我们的工程团队使用 TLA+ 来分析互联网计算机的各个方面，包括在平台上运行的安全关键智能合约。虽然以太坊和互联网计算机具有不同的执行模型，但重入错误可能出现在两个区块链的智能合约中。事实上，由于其高吞吐量，互联网计算机允许对单个智能合约进行多个并发调用，这需要智能合约作者更加小心，以消除不需要的并发交互。由于安全性对于互联网计算机的成功至关重要，因此 TLA+ 已被用于许多智能合约，以在开发阶段检测错误。最近对新发布的 Chain-Key Bitcoin (ckBTC) 罐（互联网计算机的智能合约）进行了 TLA+ 分析，我将在下面分享结果。
要谈论 ckBTC 的 TLA+ 分析，让我们从 ckBTC 的高级概述开始。 ckBTC 是一种互联网计算机本机令牌，由比特币 (BTC) 以 1:1 的比例安全支持。 ckBTC 分类帐是互联网计算机区块链上的罐式智能合约，用于跟踪每个最终用户拥有多少 ckBTC。与在比特币网络上转移 BTC 相比，这个相同的账本使最终用户能够更快、更便宜地将他们的 ckBTC 转移给其他最终用户。为了将 ckBTC 与 BTC 相互转换，最终用户与不同的智能合约进行交互，即 ckBTC 铸币机。
在高层次上，从 BTC 到 ckBTC 的转换操作如下所示：
获取ckBTC的步骤：
*免责声明：为简单起见，上述过程省略了 KYT（了解您的交易）过程
las，上面呈现的高级图片实际上隐藏了一个微妙的并发问题。好消息是我们可以使用 TLA+ 工具包检测问题。但在 TLA+ 可以检测到任何东西之前，我们必须首先为它提供两件事：
该模型是系统的简化但仍然完全定义的版本。在我们的例子中，它包括 minter 智能合约，但也包括系统的所有其他相关部分，即账本合约和比特币网络。对于每个组件，我们对其状态以及最终用户可能采取的相关操作（即转移 BTC 或 ckBTC、存入 BTC，或调用铸币者公开的不同操作）如何改变状态进行建模。所有这些元素在模型中都得到了一定程度的简化；分析关注的部分（例如铸币者代码）的建模更详细，而其他部分（例如比特币网络）的建模则不太详细。事实上，TLA+模型类似于系统的详细设计规范。
直觉上，我们想要实现的主要特性是确保我们的 ckBTC 得到充分支持。换句话说，任何最终用户都不应该能够\"双花\"他们存入的 BTC 以获得比他们存入的更多的 ckBTC。但是要分析这样的属性，我们必须通过用 TLA+ 语言正式表达它来使这种直觉非常精确。我们的正式定义是，ckBTC 的总供应量（即所有最终用户的 ckBTC 余额之和，由 ckBTC 分类账存储）不超过铸币罐控制的 BTC 总量（即，某个存款地址拥有的所有 UTXO 的值）。
一旦我们创建了模型和属性，TLA+ 工具包就可以分析模型。要运行分析，我们首先定义运行分析的设置。例如，我们对 ckBTC 的设置仅包括两个不同的最终用户，以及少量的比特币总供应量（例如，5 聪）。虽然这种设置非常有限，但实证研究表明，计算机系统中的绝大多数问题都可以通过少量实体来发现。小设置允许分析系统地探索模型定义的所有可能的动作序列，并检查规定的属性在任何此类序列下是否成立。此外，分析完全自动运行，即不需要任何人工输入。如果这些属性不成立，它会为我们提供违反该属性的确切操作顺序。
例如，分析可以发现我们可以在如下图所示的场景中违反我们的\"无无担保的 ckBTC\"属性：
这里：
因此，在第 4 步结束时，我们处于 ckBTC 供应量是存款地址中 UTXO 总和的两倍的状态，这违反了我们的\"无未支持的 ckBTC\"属性。请注意，此错误的出现只是因为并发执行了对最终用户余额的更新——它实际上是一个重入错误，与导致 The DAO 宕机的错误风格相同。
解决此问题的一种方法是防止为同一最终用户并行运行余额更新。我们可以通过让铸币商在余额更新开始时将最终用户存储在\"锁定\"用户列表中，并在更新期间将他们保留在该列表中来实现这一点。如果最终用户尝试启动另一个并发余额更新，更新将首先检查并在锁定用户列表中找到这个特定的最终用户，然后中止。
请注意，我们在这里稍微简化了攻击：锁定实际上是 IC 智能合约的一种相当常见的模式，并且 ckBTC 铸造者从一开始就部署了它。然而，锁定执行不当，为上述攻击打开了大门。 TLA+ 能够检测到这一点。此外，我们还发现了一些违反\"没有未支持的 ckBTC\"和其他重要属性的边缘案例。一旦我们应用了所有修复程序，TLA+ 就可以验证并确认在我们定义的设置中没有更多的属性违规。
绝对地！好的，好的，也许我应该提供一个更细致的答案。只要涉及非平凡的并发，我们的研发团队就会将其用于互联网计算机上的关键智能合约。例如，TLA+ 分析发现了互联网计算机治理和分类账容器中的细微并发错误，这些错误在早期的手动安全审查中被遗漏，并且可能导致重大问题。案例和要点——TLA+ 在发现此类棘手问题方面绝对大放异彩。
当然，在获取专有技术然后构建模型方面要付出一定的代价。但从经验来看，这个价格是合理的，尤其是考虑到区块链安全的高风险性。人们不应该被 TLA+ 语言本身吓倒。尽管名字吓人，但要访问其强大的功能却相当简单。事实上，描述几乎所有 TLA+ 功能的 TLA+ 备忘单大致可以放在一页纸上。
更重要的是，构建模型所需的工作量可与标准的手动安全审查相媲美。例如，对于 ckBTC 铸币者，了解设计、创建初始模型和属性总共需要 1 个人大约 3 周的时间。生成的 TLA+ 模型比实现要简洁得多，这既是因为它比代码更简单，也是因为 TLA+ 的高级性质。与数千行 Rust 实现相比，ckBTC 铸币机的模型需要大约 250 行代码。也许令人惊讶的是，就工作量而言，最困难的部分之一是指定所需的属性，因为人们经常会在直观的规范中发现差距。一旦模型完成，分析（模型检查）就会自动完成。分析可能会运行很长时间——例如，对于 ckBTC，它需要 20 多个小时才能完成。最后，TLA 的另一个好处是建模和分析可以在代码实施之前的设计阶段完成。这有助于消除后期因设计错误而导致的大型重构。
TLA+ 无用的地方从消极方面来说，TLA+ 对于复杂的顺序程序的帮助较小，与并发程序相反。它也不擅长处理复杂的加密协议。还有其他工具（例如 Tamarin）对此类协议更有用。最后，还有保持 TLA+ 模型和实际实现同步的问题；随着实现代码随着时间的推移而发展，它可能不再符合模型。如果没有工具支持，这可能很难捕捉到。事实上，我们的研发团队正在尝试解决这个问题——我希望我们能尽快与您分享一些工具！
我希望这篇概述已经激发了您将 TLA+ 用于您自己的关键智能合约的兴趣。如果是这样，请继续关注——关于如何将 TLA+ 用于智能合约的更深入教程的后续帖子即将发布，并附有我们研发团队开发的实际 TLA+ 模型。
浏览量311984
浏览量138764
浏览量113326
