Smartcheck: Static analysis of ethereum smart contracts

Smartcheck: Static analysis of ethereum smart contracts

论文题目：(2018-WETSEB)Smartcheck: Static analysis of ethereum smart contracts——以太坊智能合约的静态分析

论文引用：Tikhomirov S, Voskresenskaya E, Ivanitskiy I, et al. Smartcheck: Static analysis of ethereum smart contracts[C]//Proceedings of the 1st International Workshop on Emerging Trends in Software Engineering for Blockchain. 2018: 9-16.

工具开源： smartdec/smartcheck: SmartCheck

一、主要内容

提供了solidity的一个全面代码问题分类。此外，还完善了一个用于检测他们的扩展静态分析工具SmartCheck。

SmartCheck 将 Solidity代码转化为基于xml的中间表示式，然后根据XPath模式对其进行对比检查。通过一个现实世界中的大合约数据样本对此工具进行了评估，之后将其结果和人工审计下的三个合约结果进行比较。

Security issues

Balance equality

避免对余额进行严格的相等检查。攻击者可以通过挖矿或者自毁向任意账户发送ether。

1
2
if (this.balance == 42 ether) { /* ... */} // bad
if (this.balance >= 42 ether) { /* ... */} // good

Unchecked external call

无检查的外部调用：当发送ether时，检查返回值并处理发生的错误才是正确的做法。推荐的方法是用transfer来发送ether。

1
2
3
addr.send (42 ether); // bad
if (! addr.send (42 ether)) revert; // better
addr.transfer (42 ether); // good

DoS by external contract

条件语句不应该依赖于外部调用。如不这样，被调用方也许会永远被调用失败，以至于组织调用方完成全部执行。例子如下：

1
2
3
4
5
function dos(address oracleAddr) public {
badOracle = Oracle(oracleAddr);
if (badOracle.answer () < 42) { revert; }
	// ...
}

send instead of transfer

完成ether支付的推荐方法是send

Re-entrancy

重入漏洞

1
2
3
4
5
6
7
8
pragma solidity 0.4.19;
contract Fund {
mapping(address => uint) balances;
	function withdraw () public {
		if (msg.sender.call.value(balances[msg.sender ])())
		balances[msg.sender] = 0;
	}
}

Malicious libraries

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

1

Using tx.origin

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

1
2
3
4
5
6
7
8
9
10
pragma solidity 0.4.19;
contract TxWallet {
address private owner;
function TxWallet () { owner = msg.sender; }
function transferTo(address dest , uint amount) public
{
require(tx.origin == owner); // authentication
dest.transfer(amount);
}
}

Transfer forwards all gas.

Solidity提供了许多的方法来转移ether。推荐的方法是使用addr.transfer(x)，这样只会提供给被调用方2300gas的补贴。

Functional issues

Integer division

整数除法：Solidity不支持浮点类型和十进制类型。整数除法的商是采用四舍五入的方法获取的。在计算ether或者令牌数量的时候特别要注意。该模式在分子和分母都为数字文字的地方检查除，也就是“/”符号。

Locked money.

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

Unchecked math

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

Timestamp dependence.

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

1
if (now % 2 == 0) winner = pl1; else winner = pl2;

Unsafe type inference

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

1
for (var i = 0; i < array.length; i++) { /* ... */ }

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

1
for (uint256 i = 0; i < array.length; i++) { /*...*/ }

Operational issues

Byte array

字节数组：为了更低的gas消耗，我们会尽量采用字节而不是字节数组。该模式检测字节数组的构造。

Costly loop

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

1
for (uint256 i = 0; i < array.length; i++) { costlyF (); }

Developmental issues

Token API violation

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

1
2
3
4
5
function transferFrom(address _spender , uint _value)
returns (bool success) {
require (_value < 20 wei);
// ...
}

Compiler version not fixed.

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

  • 建议遵循后一个示例，因为将来的编译器版本可能以开发人员没有预见到的方式处理某些语言结构。该模式检测pragma指令中的版本操作符。

private modifier

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

Redundant fallback function.

冗余的回退功能：合同应该拒绝未预期的付款。在solidity 0.4.0之前，这项工作都是通过手动完成的：

  • 从solidity0.4.0开始，从solid 0.4.0开始，没有回退功能的契约将自动恢复支付，从而使上面的代码变得多余。该模式检测所描述的构造(仅当pragma指令指示编译器版本不低于0.4.0时)。
1
function () payable { throw; }

Style guide violation

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

1
2
3
4
function Foo(); // bad
event logFoo (); // bad
function foo(); // good
event LogFoo (); // good

Implicit visibility level

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

1
2
3
function foo() { /*...*/ } // bad
function foo() public { /* ... */ } // good
function bar() private { /* ... */ } // good

二、设计实现

使用的是一款java系的静态分析Ethereum智能合约的工具。

SmartCheck在可靠的源代码上运行词法和句法分析，它使用了ANTLR和一套Solidity自定义的语法来生成一棵XML解析树。

通过在IR上使用XPath [xpa]查询来检测漏洞模式。因此，SmartCheck提供了全面的覆盖:分析的代码被完全转换为IR，所有元素都可以通过XPath匹配获得。行号作为XML属性存储，并帮助在源代码中本地化结果。当实现新的分析方法时，IR属性可以通过附加信息得到丰富。

image-20201126195029448

Figure 1: Parse tree for the Balance equality code example

三、实验评估

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

在具体实验中，我们将SmartCheck和另外三种静态检测工具Oyente、Remix和Security进行了比较。将一个真的检测结果看作需要解决的问题。工具发现的所有问题都手工标记为true positive (TP)或false positive (FP)。

对于这四个工具(Oyente、Remix、Securify和SmartCheck)，每个工具的假阴性(false negative, FN)都是这个工具没有检测到的真实结果。对于每个工具

  1. 错误发现率FDR：$FDR = \frac{FP}{TP + FP} $，是该工具的FPs数量除以该工具报告的所有问题的数量
  2. 假阴性率(False negative rate, FNR)：$FNR = \frac{FN}{TP + FN} $，是该工具的FN个数除以所有真实结果(由任何工具或手动发现)的个数

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

Table 2：Tools results on the three projects and overall

image-20201126195353156

四、总结评价

主要贡献；

  • 对于在solidity中已知的可靠代码问题进行了全面的概述和分类
  • 实现了一个有效的静态分析工具SmartCheck

一些不足：

  • SmartCheck也有其自身的局限性，当检测一些错误时需要更加复杂的技术，例如污染分析或甚至人为审核。