论文：Sergei Tikhomirov, Ekaterina Voskresenskaya, Ivan Ivanitskiy, Ramil Takhaviev, Evgeny Marchenko , Yaroslav Alexandrov. SmartCheck: Static Analysis of Ethereum Smart Contracts

SmartCheck:以太坊智能合约的静态分析_合约_对象 云服务

2018 IEEE/ACM 1st International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB)

http://orbilu.uni.lu/bitstream/10993/35862/1/smartcheck-paper.pdf

论文择要：

以太坊是一个基于区块链的智能合约平台。
Solidity是个中最成熟的高等合约措辞。
以太坊也是一个针对那些企图利用漏洞获利的不法分子有所戒备的实行平台。
开拓者对付已支配的左券每每很难进行修正。
黑客们可从具有漏洞的合约中盗取数千万美元，个中一个非常著名的例子便是2016年6月的“The DAO”。
在博客、论文和教程中随处可见关于以太坊编程实战的安全建议。
由于这一领域的快速发展，许多资源都已经由时。
那些帮助检测潜在问题措辞构造的自动漏洞检测工具仍旧有待发展。

我们供应了solidity的一个全面代码问题分类。
此外，还完善了一个用于检测他们的扩展静态剖析工具SmartCheck。
SmartCheck将Solidity代码转化为基于xml的中间表示式，然后根据XPath模式对其进行比拟检讨。
我们通过一个现实天下中的大合约数据样本对此工具进行了评估，之后将其结果和人工审计下的三个合约结果进行比较。
我们的工具反响了在Solidity漏洞上确当前状态也展示了其与替代工具比较的进步。
当然，SmartCheck也有其自身的局限性，当检测一些缺点时须要更加繁芜的技能，例如污染剖析或乃至人工审计。
我们始终坚信，一款好的静态剖析器应该在合约开拓者工具箱中拥有一个主要的地位，从而让他们办理大略问题时更加的迅速，也有更多的精力来办理繁芜问题。

以太坊先容：Ethereum于2014年推出，2015年推出[VB+14]。
Ethereum节点利用类似于比特币的事情证明共识机制存储数据、实行智能左券并掩护环球状态的共享视图[Tik17]。
与以前区块链编程(如比特币脚本)的考试测验相反，Ethereum措辞是图灵完备的，因此能够表达任意繁芜的逻辑。

面临寻衅：

陌生的实行环境：代码运行在环球网络的节点中，而这些节点又是具有匿名的,缺少信赖,惟利是图的特点

新的软件栈：仍处于开拓中，无法确保有隐蔽的漏洞涌现

修正支配的合约非常困难

充满了受金钱诱惑、蠢蠢欲动的潜在罪犯

快速的发展

Solidity本身不是一个令人最满意的措辞发射点

我们将Solidity中代码的问题分为如下种别：

安全问题：

1. 余额相等：避免对余额进行严格的相等检讨。
仇敌可以通过挖矿或者自毁向任意账户发送ether。

2. 无检讨的外部调用:当发送ether时，检讨返回值并处理发生的缺点才是精确的做法。
推举的方法是用transfer来发送ether。

3. 条件语句不应该依赖于外部调用。
如不这样，被调用方大概会永久被调用失落败，以至于组织调用方完玉成体实行。
例子如下：

4. 完成ether支付的推举行法是addr

5. 对付上述合约，在msg.sender处可以得到多个资金并在他的份额降落到0前通过循环调用withdraw来规复所有Fund的ether。

6. 恶意的库。
第三方库可能是恶意的。
避免外部依赖或确保第三方代码只包含预期的功能。
该模式只是检测library关键字

7. 利用 tx.origin 。
合约可以相互调用公共方法。
Tx.origin是在调用链中的第一个账户。
Msg.sender是中间的调用方。
举个例子，在一个A->B->C的这样一个调用链中，从C的角度来看，tx.origin 是A,msg.sender 是B。

8. 转移所有的gas。
Solidity供应了许多的方法来转移ether。
推举的方法是利用addr.transfer(x)，这样只会供应给被调用方2300gas的补贴。

功能问题：

1. 整数除法：Solidity不支持浮点类型和十进制类型。
整数除法的商是采取四舍五入的方法获取的。
在打算ether或者令牌数量的时候特殊要把稳。
该模式在分子和分母都为数字笔墨的地方检讨除，也便是“/”符号。

2. 加锁的钱：为接管ether而编写的合约应该同时完善一个撤回ether的方法，即，至少一次的transfer,send,call.value。
该模式检测包含支付功能但不包含上述取款功能的合约。

3. 无检讨的数学打算：solidity易涌现整数的上溢和下溢。
上溢将导致无法预见的、可能被恶意账户利用导致资金丢失的影响。
利用SafeMath library检讨上溢。
该模式能够检讨不包含在条件语句中的算数运算“+”和“-”。
由于假阳性率较高，这一条规则被暂时在第四节测试时被取消了。

4. 对韶光戳的依赖：矿工可以操纵环境变量并且如果有机会从中获利的话有可能会这么做。

矿工可以通过调度韶光戳来得到不公正的上风。
利用块号和块之间的均匀韶光来估计当前的韶光。
利用安全的随机性源。
该模式检测当前的环境变量。

5. 不屈安的类型推断。
Solidity支持类型推断:var i = 42中的i类型;是能够存储右侧值(uint8)的最小整数类型。
类似如下循环:

该类型的i是unit8，如果array.length的长度超过了256就会涌现上溢的问题。
我们须要像下例一样平常在声明整数变量时准确定义其类型：

操作问题：

1. 字节数组：为了更低的gas花费，我们会只管即便采取字节而不是字节数组。
该模式检测字节数组的布局。

2. 高代价的循环：Ethereum是一个资源有限党的环境。
每一个打算步骤的价格都要比集中式云供应商高几个数量级。
此外，Ethereum 的矿工对一个区块的gas小号都有个限定。
不才述例子中，如果array.length足够大，也便是函数超过了快gas的限定，调用他的事务将永久不会被确认：

如果外部参与者影响array.legnth,这就会引发一个安全问题。
例如，如果数组列举所有注册地址，且注册是开放的，则对手可以注册多个地址，从而导申谢绝做事。
该规则包括两种模式:

•for语句，条件内带有函数调用或标识符;

•条件内带有函数调用的while语句。

开拓问题：

1． 违反令牌API：ERC20是实现令牌的实际标准API。
Exchanges和其他第三方做事可能难以集成不符合他的令牌。
对付某些返回bool的ERC20函数，不建议在期中抛出非常。

该模式检测从名称包含单词“token”的合约继续而来的合约，该名称可能会从上述函数中抛出非常。

2． 变动的编译器版本：Solidity源文件可以表明编译器的版本

建议遵照后一个示例，由于将来的编译器版本可能以开拓职员没有预见到的办法处理某些措辞构造。
该模式检测pragma指令中的版本操作符。

3． 私有化转换：与普遍的认知相反，私有化转换不是使一个变量不可见。
挖矿者可以访问所有合约的代码和数据。
开拓者必须承认的是Ethereum存在着缺少隐私的问题。
该模式检测带有私有润色符的状态变量声明。

4． 冗余的回退功能：条约该当谢绝未预期的付款。
在solidity 0.4.0之前，这项事情都是通过手动完成的：

从solidity0.4.0开始，从solid 0.4.0开始，没有回退功能的左券将自动规复支付，从而使上面的代码变得多余。
该模式检测所描述的布局(仅当pragma指令指示编译器版本不低于0.4.0时)。

5． 违反风格规范：在solidity中，function9和事宜的名称常日都以小写和大写字母开头

违反风格规范会降落可读性并导致混乱。
模式检测所描述的构造。

6． 隐式能见度水平。
在稳定性中，默认的函数可见性级别是public。
显式定义函数可见性以防止稠浊。

工具先容：

在本文中，我们利用的是一款java系的静态剖析Ethereum智能合约的工具。
SmartCheck在可靠的源代码上运行词法和句法剖析，它利用了ANTLR和一套Solidity自定义的语法来天生一棵XML解析树。
我们通过在IR上利用XPath [xpa]查询来检测漏洞模式。
因此，SmartCheck供应了全面的覆盖:剖析的代码被完备转换为IR，所有元素都可以通过XPath匹配得到。
行号作为XML属性存储，并帮助在源代码中本地化结果。
当实现新的剖析方法时，IR属性可以通过附加信息得到丰富。

该工具同时也可通过添加指定语法和数据库扩展支持其他智能合约。

在详细实验中，我们将SmartCheck和其余三种静态检测工具Oyente、Remix和Security11进行了比较。
我们将一个真的检测结果看作须要办理的问题。
工具创造的所有问题都手工标记为true positive (TP)或false positive (FP)。
对付这四个工具(Oyente、Remix、Securify和SmartCheck)，每个工具的假阴性(false negative, FN)都是这个工具没有检测到的真实结果。

对付每个工具，缺点创造率(FDR)是该工具的FPs数量除以该工具报告的所有问题的数量:FDR = FP / (TP + FP)。
假阴性率(False negative rate, FNR)是该工具的FN个数除以所有真实结果(由任何工具或手动创造)的个数，即该工具的TP和FN之和:FNR = FN / (TP + FN)。

个中对付3个合约Genesis、Hive和Populous的测试结果如下所示:

此外，smartcheck还在大样本上进行了测试，共4600个合约，剖析耗时7644秒，结果如下：

本文紧张贡献：对付在solidity中已知的可靠代码问题进行了全面的概述和分类实现了一个有效的静态剖析工具SmartCheck,与现有的替代方案比较有了明显的升级进步。
致谢

本文由南京大学软件学院2016级本科生徐介晖翻译转述