论文：谢尔盖蒂霍米罗夫、叶卡捷琳娜沃斯克里森斯卡娅、伊万伊万尼茨基伊、拉米尔塔克哈维耶夫、叶夫根尼马尔琴科、雅罗斯拉夫亚历山德罗夫。以太坊智能合约的静态分析
2018 IEEE/ACM首届区块链软件工程新兴趋势国际研讨会(WETSEB)
http://or bilu . uni . Lu/bitstream/10993/35862/1/smart check-paper . pdf
以太坊是一个基于区块链的智能合约平台。Solidity是最成熟的高级契约语言之一。以太坊也是那些企图利用漏洞牟利的罪犯的行刑平台。开发人员通常很难修改已部署的契约。黑客可以从易受攻击的合同中窃取数千万美元，其中之一是2016年6月的“The DAO”。关于以太坊实用编程的安全建议，在博客、论文、教程中随处可见。由于该领域发展迅速，很多资源已经过时。那些帮助检测潜在问题的语言结构的自动漏洞检测工具仍然需要被开发。
我们为solidity提供了代码问题的全面分类。此外，扩展的静态分析工具SmartCheck经过改进可以检测它们。SmartCheck将Solidity代码转换成基于xml的中间表达式，然后按照XPath模式进行比较。我们通过一个真实世界的大型合同数据样本来评估这个工具，然后将其结果与人工审计下的三个合同的结果进行比较。我们的工具反映了坚固性漏洞的当前状态，并显示了它与替代工具相比的进步。当然，SmartCheck也有自己的局限性。在检测一些错误时，需要更复杂的技术，比如污染分析甚至人工审计。我们始终认为，一个好的静态分析器应该在契约开发者的工具箱中占有重要的位置，这样他们才能更快地解决简单的问题，有更多的精力去解决复杂的问题。
以太坊简介：以太坊于2014年和2015年推出。以太坊节点存储数据，执行智能合约，并使用类似于比特币的工作证明共识机制来维护全球状态的共享视图。与之前区块链编程的尝试(如比特币脚本)相反，以太坊语言是图灵完备的，因此可以表达任意复杂的逻辑。
陌生的执行环境：代码运行在全球网络的节点中，这些节点的特点是匿名、缺乏信任和逐利。
新的软件栈：还在开发中，没有办法保证有隐藏的漏洞。
修改已部署的合同非常困难。
充满了受金钱诱惑的潜在罪犯。
迅速发展
扎实本身并不是最令人满意的语言发动点。
我们将代码在可靠性方面的问题分为以下几类：
安全问题：
1.天平平等：避免对天平进行严格的平等检查。敌人可以通过采矿或自我毁灭把以太送到任何账户。
2.发送以太时不检查3360的外部调用，检查返回值并处理发生的错误才是正确的做法。推荐的方法是用传送送乙醚。
3.条件语句不应该依赖外部调用。否则，被调用者可能被永远调用而失败，这样调用者被组织起来完成所有的执行。例子如下：
4.完成乙醚支付的推荐方法是addr。
5.对于上述合同，可以在msg.sender处获得多笔资金，在他的份额减少到0之前，可以通过循环调用withdraw来恢复所有资金的乙醚。
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。显式定义函数可见性以防止混淆。
该工具同时也可通过添加指定语法和数据库扩展支持其他智能合约。
在具体实验中，我们将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秒，结果如下：
