从最初的 “The DAO” 智能合约开始，重入漏洞就一直困扰着各种区块链上的智能合约，随后，又发生了一系列备受瞩目的漏洞，智能合约中数亿甚至数十亿美元的资金被盗。
这些漏洞很难通过测试发现，因为它们只在智能合约代码的不同部分按特定顺序执行时才会出现，此类顺序的数量非常庞大，因此简单的测试无法实现。
在之前的博客文章中，我们展示了如何使用 TLA+（一个能够全面测试软件设计的通用工具包）进行形式化验证，有效地消除互联网计算机上智能合约（或称“容器”）中的重入漏洞。
这些博客文章如下：
使用 TLA+ 消除智能合约错误：介绍 TLA+，使用 ckBTC 案例研究来说明模型检查如何查找并帮助修复可重入错误。
使用 TLA+ 模型清除错误：了解 DFINITY 的开源 TLA+ 模型（NNS、ckBTC 等）以及面向开发人员的真实示例。
教程 - 使用 TLA+ 制作互联网计算机容器：有关如何使用 TLA+ 和 PlusCal 建模互联网计算机容器并检查其属性的分步技术指南。
虽然我们发现 TLA+ 在消除重入错误方面非常有效，但它的使用存在一个局限性：TLA+ 模型对应于某个时间点的代码快照，但随着代码的演进，这些模型可能会过时，甚至可能无人察觉，重入错误可能会再次出现在代码库中。
在本文中，我们提出了一种解决这个问题的方法：一个自动化框架，用于测试 Rust 容器与其 TLA+ 规范之间的一致性。
TLA+ 和同步挑战
在 TLA+ 方法中，我们不是直接测试代码，而是构建代码的简化模型，然后，我们指示 TLA+ 工具（即 TLC 模型检查器）系统地检查模型中所有可能的执行序列（直至达到一定范围），并确保无论序列如何，某些提供的属性都成立。
例如，在神经网络（NNS）治理模型中，我们可以检查神经元的投票权是否正确基于其质押的 ICP，然后，TLC 可以发现任何可重入漏洞，这些漏洞的执行序列可能允许攻击者获得更多投票权，或者实际上告诉我们不存在此类漏洞。
这种方法的一大优势是 TLA+ 模型比代码更简单，无需人工输入即可有效分析模型，正因如此，一些科技巨头，例如微软和 AWS，也使用 TLA+ 来验证其关键基础设施。
然而，验证保证仅适用于模型，而不适用于代码本身，虽然可以有效地手动检查模型与代码的一致性，但随着代码的演变，这项工作变得繁琐乏味，每次代码更改都可能需要检查模型是否仍然能够正确捕获代码。
因此，模型和代码往往会随着时间的推移而失去同步，这意味着在创建和检查模型时提供的强一致性保证最终会消失。
这正是我们在最近的一个功能中解决的问题，我们开发了一个框架，用于自动测试 Rust 容器代码与其 TLA+ 模型之间的对应关系，并将其应用于我们的治理容器，现在，我们的 CI（持续集成）流水线会持续测试治理代码是否与模型存在偏差。
这让我们和更广泛的 ICP 社区能够安心，因为 NNS 是安全的，并且能够抵御任何试图通过重入漏洞实现 NNS 接管的攻击者，此外，该框架并非特定于治理：它可以应用于其他互联网计算机容器，包括社区容器。
工作原理
TLA+ 模型将系统描述为过渡系统，在此类系统中，所谓的过渡谓词描述了系统如何将其状态从一个状态转换为另一个状态，当谓词对两个状态 s1 和 s2 为“真”时，系统可以从状态 s1 转换为 s2，如果谓词对 s2 和某些 s3 也为“真”，则系统可以从 s1 转换为 s2，再转换为 s3，依此类推。
给定过渡谓词和另一个指定哪些状态是有效起始状态的“初始”谓词，模型检查器可以构建所有有效的状态序列（也称为轨迹），此外，用户可以指定一个谓词来定义“好”状态和“坏”状态，然后模型检查器可以在通过某些有效的状态序列达到坏状态时发出警报。
这和我们的容器有什么关系？容器在处理消息时会改变状态，这些消息可以是用户消息、来自其他容器的消息，也可以是系统生成的“心跳”或“计时器”消息，消息由所谓的消息处理器处理。
由于 ICP 保证消息处理器的执行是原子的，我们可以在 TLA+ 中对容器进行建模，方法是将转换谓词定义为“相关容器的某个消息处理器已执行”，并在 TLA+ 谓词中定义我们认为每个消息处理器执行的操作。
那么问题是：我们是否在 TLA+ 中正确捕获了消息处理程序实际执行的操作？
为了解答这个问题，我们构建了一个工具，可以复用现有的容器测试，从此类测试执行中收集状态对，每个收集到的状态对描述了容器在每个消息处理程序开始和结束时的状态，或者至少描述了与 TLA+ 模型相关的状态部分（具体哪些相关由用户决定）。
现在，我们可以调用 TLA+ 模型的转换谓词，并询问：我们观察到的状态对是否真的满足谓词？如果不满足，那么我们就知道代码做了一些 TLA+ 模型未考虑到的事情，并发出警报（导致 CI 失败）。
如上所述，随着代码的不断发展，这一点尤为重要：现在，导致 TLA+ 模型与代码不兼容的意外更改有机会被自动检测到。
工作量有多大？
该工具需要三个主要步骤：
构建 TLA+ 模型本身。
对 Rust 容器代码进行插桩，以检测每个消息处理程序的开始和结束，并描述如何将容器状态映射到 TLA+ 值，插桩可以分为两种类型：散布在整个生产代码中的插桩，以及保存在单独模块中的插桩，我们专注于精简第一种类型的插桩，例如，对于治理而言，添加到生产代码中的代码不超过 100 行，虽然我们没有专注于保持第二种类型的插桩精简，但此类代码仍然不超过 1000 行。
对测试进行插桩，以调用检查记录状态是否满足转换谓词的函数，对于仅使用 Rust 的测试（即没有构建实际的 Wasm 容器并将其上传到副本），每个测试只需一行代码即可完成此操作，对于基于 Wasm 的测试，需要进行一些额外的工作来通过查询来公开和获取记录状态，但每个测试也只需一行代码。
有关如何设置工具的更详细的技术说明可在 IC GitHub 存储库中找到。
结论
此工具专注于提供一种廉价而有效的方法，用于检查模型与 Rust 容器代码之间的对应关系，然而，它只能根据您已编写的测试中观察到的情况来检测偏差，它无法检测仅在未经测试的场景下才会发生的偏差。
因此，通过这种方式获得的保证，相比其他一些验证方法（尤其是代码级验证）获得的非常强的保证，要弱得多。
然而，与编写 TLA+ 模型、自动进行模型检查以及使用提供的工具对代码进行插桩相比，代码级验证也更加费力，我们相信，这种方法在所需的工作量和所提供的收益之间找到了一个最佳平衡点。
此外，它与测试具有协同作用：测试覆盖率越高，您就越能确信您的代码与 TLA+ 模型同步，从而避免出现重入错误。
如果您已经开始为自己的容器编写 TLA+ 模型，则可以从IC 存储库中获取将模型链接到代码的工具（包括文档）。
否则，如果您刚刚开始为自己的容器使用 TLA+，这里有一些有用的资源：
我们的博客文章介绍了 TLA+ 如何以及为何有助于防止重入漏洞；
使用 TLA+ 建模互联网计算机容器的技术教程或视频（第 1 部分、第 2 部分）；
免费提供的 TLA+ 资源：《学习 TLA+》一书、《指定系统》一书、TLA+ 视频课程；
Internet Computer 关于 TLA+ 的文档页面。
你关心的 IC 内容
技术进展 | 项目信息 | 全球活动
收藏关注 IC 币安频道
掌握最新资讯
