Securify: Practical Security Analysis of Smart Contracts

Securify: Practical security analysis of smart contracts

论文题目：(2018-CCS) Securify: Practical security analysis of smart contracts

论文引用：Tsankov P, Dan A, Drachsler-Cohen D, et al. Securify: Practical security analysis of smart contracts[C]//Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. 2018: 67-82.

代码开源： crytic/slither

一、主要内容

Securify是一个全自动化，并且可扩展的分析智能合约，检测漏洞的工具。Securify基于模式匹配。其能在给定特征的情况下分析智能合约是否存在漏洞。

Securify 的分析针对字节码（bytecode），即智能合约源代码（solidity语言）被编译后的结果。通过对bytecode的分析，得出dependency graph，进而得到合约的语义信息。之后根据给定的特征分析合约语义信息是否满足遵循或违背这些特征，判断合约是否存在漏洞。

Securify的输入为智能合约的bytecode或源代码（被编译成bytecode输入工具）以及一系列模式，模式采用domain-specific language（DSL，领域特定语言）描述。输出为具体出现漏洞的位置。用户可以自己书写模式，因此Securify有可扩展性。

二、MOTIVATION EXAMPLES

Stealing Ether

以下是一个存在漏洞的具体合约。红色标明的部分为漏洞存在的地方

image-20201126192221139

Figure 3：A vulnerable wallet that allows any user to withdraw all ether stored in it

由于函数默认的访问限制为public，因此initWallet()函数默认可以被外部调用（向该合约发送交易），导致任何人都可以更改钱包的所有者。

Securify的模式有两大类，compliance & violation；对应上述的合约，Securify可以匹配出violation pattern为owner的赋值不依赖于交易的发送者。那么对应的安全特征为owner的写入是必须受限的。

Frozen Funds

deposit函数有关键字payable，表明交易发送者可以通过调用该函数来向这个合约转账。这个合约的漏洞在于，它本身没有向其他账户转账的函数，实现的功能是通过调用别的合约作为library实现的。而合约可以被销毁。那么假设有一个攻击者销毁了library，那么调用这个library来实现转账的那个合约里面的资产会被全部冻结。

image-20201126192450461

Figure 4: A wallet that delegates functionality to a library contract walletLibrary

匹配该漏洞的violation pattern为：

  1. 用户可向合约存钱，即stop指令（调用结束指令）不依赖于转账的以太币为0（即可以向合约成功存钱）
  2. 对于所有的call指令（调用函数指令），转出的以太币为0（即合约本身没有能力向外转出钱）

三、THE SECURIFY SYSTEM

本部分展示整个系统的实现：

  1. 绿色部分指代输入，即EVM bytecode and security patterns
  2. 红色部分指代输出，即a violated instruction
  3. 灰色框代表中间分析工件（intermediate analysis artifacts）

Securify分三个步骤进行：

  1. 将合同的EVM字节码反编译（decompiles）为静态单分配形式（static-single assignment form）；
  2. 推断有关合同的语义事实（semantics facts）；
  3. 匹配合同上受限写属性（restricted write property）的违反模式（the violation pattern）。

image-20201126192828618

Figure Figure 5: High-level flow illustrating how Securify finds the unrestricted write to the owner field of the contract

INPUTS

  1. 合约的bytecode或者solidity源代码（编译成bytecode）
  2. patterns，用DSL描述

Decomplie

bytecode在以太坊虚拟机EVM上运行。EVM是一个基于栈的虚拟机。

Securify将基于栈运行的bytecode转换为不基于栈的SSA表达形式，具体做法未详细给出。

之后恢复CFG，其中针对Securify的整体分析方法做了一些优化。

Inferring Semantic Facts

该部分Securify分析合约的 semantic facts，使用Datalog描述。整个过程使用已有的Datalog Solver全自动化工具。分析包含了数据依赖和控制依赖。

首先Securify分析针对指令分析出base fact，比如说

l1: a = 4 分析得到

assign(l1, a, 4)

之后，分析每一个指令后，将得到的所有base facts输入到已有的工具，推断出进一步的语义信息，即semantic facts。

Checking Security Patterns

patterns使用securify自己的语言描述。模式匹配时，Security 迭代指令，处理含有some和all量词的pattern，以及，为了检查推断出的facts, Securify直接向Datalog Solver查询。Securify的模式匹配局限之处为：安全特征比较宽泛，没有对具体的合约分析

四、实验评估

作者主要进行了一下几个实验

  1. 对真实的合约做分析，评估Securify的有效性
  2. 将Securify与Oyente和Mythril（两个已有智能合约分析工具）比较
    • 注意Oyente和Mythril均是基于符号执行的，因此被这两个工具分析出的结果是必定会被执行到的
  3. 评估Securify对memory和storage的分析结果
  4. 取得Securify分析时的时间和内存消耗

作者使用的数据集有两个

  1. 约25K的bytecode数据集（EVM dataset）
  2. 100个solidity数据集（solidity dataset）

image-20201126191157161

Figure 11: Securify results on the EVM dataset

五、总结评价

主要贡献：

  1. 使用反汇编Datalog描述智能合约
  2. 通过compliance 和 violation的pattrn，来检查给定安全特征是否满足
  3. 提出了Securify这个工具

一些不足：

  1. Securify比已有的两个工具效果好很多，可是Securify的基本方法和这两个工具不同，比较不是很令人信服。