智能合约分析器在Zilliqa中发挥了什么作用？

智能合约为在区块链上实施业务逻辑提供了方法。与大多数企业一样，智能合约通常涉及大量的资金处理（通常是数亿美元）；“money”就是该平台的原生代币，例如Zilliqa的ZIL，以太坊的ETH等。比如说，在kickstarter合约中，backer向合约转账以帮助项目启动。或在拍卖合约中，竞标者将钱转到充当拍卖商的合约中，最终最高出价者为赢家。

 

由合约持有或转移到合同的资金通常经过多次转换和检查，以强调底层代码的完整性。资金也可以通过内部变量和运营商在合约中“流动”，并且必须确保过程安全以及一致。

当然，不受限制的资金流动可能会导致资金损失。此外，由于区块链是不可变的，智能合约中的bug无法修补，尤其是“资金”处理方面的bug。因此，准备完善至关重要。但事实证明，大多数现有的智能合约确实存在漏洞，导致合约中的资金被窃取或冻结。

Scilla是我们为Zilliqa设计的新型中级智能合约语言，它填补了其中一些缺陷。Scilla的一个好处是，它使编写静态分析程序变得更容易，可以在应用上线之前识别潜在的bug。利用该语言设计，我们使用Scilla编写了首个智能合约现金流分析器。该分析器允许开发人员在合约部署前跟踪和标记智能合约中的（即ZIL）的资金使用情况。这样就可以识别出应用中可能发生的资金泄漏、错误处理或盗用的代码错误，任何一个错误都可能产生破坏性的结果。

为了充分理解现金流分析器的强大功能，我们先来尝试手动查找资金（错误）处理合约中的bug，看看你是否能找出。提示：bug修复需要更改合约中的单个字符。

注意，现金流量分析器可自动检测出该合约存在的问题。

稍后我们将详细介绍现金流分析器的工作流程，以及现金流分析器如何报告以上合约中的bug。

要试用该分析器，必须使用scilla-checker二进制文件，该二进制文件可以从Scilla GitHub存储库上提供的源代码构建。我们计划在Savant IDE中添加对它的支持，方便智能合约开发人员在合约上使用。

如果你有任何疑问，或想了解如何在Scilla上开发自己的智能合约应用，请通过我们的技术论坛或一下社交渠道联系我们。

Forum：https：//forum.zilliqa.com/

Gitter：https：//gitter.im/Zilliqa/（与D开发相关的主题，包括生态系统拨款）

Telegram：https：//t.me/zilliqachat

Slack：https：//invite.zilliqa.com/

Twitter：https：//twitter.com/zilliqa

Reddit：https：//www.reddit.com/r/zilliqa/

Github：https：//github.com/Zilliqa/zilliqa

Scilla合约快速入门

在介绍现金流分析器细节之前，让我们先熟悉一下Scilla合约的基本结构。每个Scilla合约都包含以下关键部分：

1.不可变参数：这些是部署合约时的初始化变量。初始化后，其值不能更改。

2.可变状态变量：这些状态变量表示给定时间点的合约状态。可以通过调用转换来更改这些字段的值。

3.转换：这些函数允许更改可变字段的值。

4.局部变量：这些变量是在转换中声明的变量，用于操作不可变参数或字段，或执行数学计算。

5.隐式“money”变量：Scilla合约中存在一个隐式定义的状态变量_balance，用于存储合约的当前余额。此外，使用特殊变量_amount处理任何转进或转出的钱。

6.隐式“非money”变量：Scilla合约中存在几个隐式定义的“非money”变量。这些包括：_sender、调用此合约的调用者（它代表帐户地址，不代表money）、_this_address、合约地址、_recipient，用户帐户或合约希望通信的合约帐户的地址等等。

现金流分析器深度解析

现金流分析器是一种静态分析工具，它试图跟踪给定合约中ZIL的使用情况。该工具将智能合约代码作为输入，并以静态方式返回分析结果。静态意味着该工具根本不执行合约代码。

分析结果为合约不同部分的一组标记，每个标记表示每个合约特定部分处理ZIL的方式。如果标记表示使用不一致，或者标记不符合开发人员的意图，则合约中可能存在bug，不应以其当前形式进行部署。

该分析器使用基础方法进行特定领域的静态分析（称为抽象解释），这种方法已被用于多个其他属性，例如Facebook Infer的大规模数据竞争检测。

标记用途

现金流分析假设，如果一个局部变量或一个字段，以某种方式在合约某一部分表示ZIL数量，则该变量应表示合约所有部分的ZIL数量。因此，分析器为合约中的每个字段、不可变参数和局部变量分配单独标记。

每个标记表示已收集的、与被标记主体有关的ZIL相关信息。现金流分析器使用一些基本标记来表示此信息。5个基本标签如下：

1.NoInfo：没有收集到有关的ZIL相关信息。

2.Money:：用于直接表示ZIL数量。

3.NotMoney：用于表示ZIL以外的其他内容。

4.Inconsistent：有时用于表示ZIL，有时用于表示ZIL以外的其他内容。

5.Map t：Map的共域标记为t，t可以是上述标记之一。假设Map键表示除ZIL以外的其他内容。

下图为示例合约，以我们对合约的直观理解来手动标记合约的不同部分。假设此直观标记为正确的。如果合约正确处理资金，那么分析器应返回我们直观分配给代码不同部分的相同标记。

从直观到自动化

从直观标记转向自动化标记显然是一个很大的飞跃，因为分析器没有任何上下文信息可以按以上例子的方式那样分配标记。因此分析器必须从代码本身提取信息，然后使用这些信息为代码各个部分分配标记。

分析需要通过多次合约代码。在分析的最初阶段，任何字段、参数或变量都是未知的。因此，所有内容最初的标记都为NoInfo。然后分析器继续分析合约中的每个变量，决定如何使用标记主体。如果合约代码中的任何部分使用了未曾出现的标记主体，则更新该主体标记。

完成合约代码的完整遍历后，分析将检查合约的所有主体是否已更新其标记。如果出现未更新的情况，则更新标记后再次遍历合约。直到完全遍历为止，直至无标记需更新。

根据主体的使用方式来更新主体标记。提供变量信息的两个基本用途是读取和写入隐式“money”和“非money”变量。本文前半部分提到过，这些变量是语言结构，它们是否处理资金不再赘述。

为了说明分析如何从输出消息中提取信息，请考虑下图示例。该示例构造了一个包含4个字段的消息，分别为_tag、_recipient、_ount以及_custom。如图所示，与隐式变量绑定的局部变量具有与隐式变量相同的标记。

同样，从隐式变量中读取时可提取信息：

该示例从4个不同的隐式变量中读取。 前两个：_amount和_sender是调用当前转换消息的一部分。_amount字段包含传输到当前合约的ZIL数量，_sender字段包含消息发送者的地址。因此，x为Money，y在此处为NotMoney。

最后两个是所有合约中都存在的隐式状态变量。_balance字段包含合约帐户中的ZIL数量，_this_address字段包含合约地址。因此在此示例中，z为Money，w为NotMoney。

结合标记

变量的其他用途会产生更复杂的标记更新。例如以下语句中，添加变量y和z的值，并将结果存储在变量x中：

如果x，y和z未知，则无法从该语句中提取任何信息。

但假设我们知道x被标记为Money，即x用于表示合约中其他部分的ZIL。唯一能合理添加两个变量并得到一定Zil的方法是，如果这两个变量都表示ZIL数量，那么如果x被分配了Money标记，则y和z也应如此。同样，如果y或z被分配了Money标记，那么其他两个变量也是如此，因为将一定数量的ZIL添加到与ZIL无关的变量中是无意义的，并且添加两次ZIL，其数量也是一定的。

如果已为其中一个变量分配了NotMoney标记，则应用的参数也类似。添加两个变量的结果不是ZIL数量的唯一方法是，如果两个变量都不代表ZIL数量，并且将不是ZIL数量的东西添加到另一个变量的唯一方法是，其他变量也不代表ZIL数量。

测试分析器

现在我们已经了解了现金流分析器的工作原理，接下来尝试在前面的buggy合约上测试它，看看分析器是否能够检测到bug。运行分析器很简单，使用带有-cf标记（用于现金流分析器）的二进制scilla-checker并将合约文件作为输入。需要-libdir标记通知检查器读取合约中导入库的位置。

分析器返回JSON格式的结果，列出了每个状态变量的推导标记。

错误分析。分析器将变量计数标记为Money，将变量backer标记为Map Money。backer在帐户地址与ZIL存储金额之间存储映射。因此，backer的标记与合约上的上下文知识相匹配。但count是计算backer数量的简单计数器。因此，它不应被标记为Money。这意味着合约中存在一个bug，count被直接或间接用于处理资金。

现在，为使bug归零，再来看看合约。在转换buggy_withdraw（）中，有语句c < -  counter，将counter的当前值读入c。到目前为止一切顺利。

如果我们在代码中再深入一点，就会看到在构造msg时使用了c。这里出现了以下代码:_amount: c。由于_amount是一个隐式资金变量，c获取最终流向counter的标记Money，并将其标记为Money。

此时显而易见，c表示counter的当前值，因此不对应于backer应该能够提取的金额。恭喜你找到了bug！

Bug修复

正如前面所说的，Bug修复实际上需要更改代码中的一个字符。事实上，a在一个分支中代表的是backer可以提取的资金。因此，代码_amount: c应替换为_amount: a。

我们对合约进行了此更改，然后在固定合约上重新运行分析器。更改后，分析器现在可以正确地将count标记为NoInfo，因为它没有足够信息来推断count是否代表资金。

结论

本文介绍了现金流分析器，它可以检测Scilla合约中有关如何处理转入和转出资金的不一致性。分析器现在可供大家使用。但分析器有个局限性，即它主要处理原生代币，即ZIL。它不处理其他形式的货币，例如可替代代币。

但可以通过告诉分析器哪些变量可以被视为资金，来给分析器一些提示。有了开发人员的提示，现金流分析器就可以照常运行了。分析器目前已添加了此功能。

原文：https://blog.zilliqa.com/introducing-the-zil-cashflow-smart-contract-analyser-ded8b4d84362 作者：Amrit Kumar 编译：Alonso 稿源（译）：https://first.vip/shareNews?id=1564&uid=50704 如有转载，请注明出处！

来源链接：https://www.8btc.com/media/406008
转载请注明文章出处