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