Securify: Practical Security Analysis of Smart Contracts

发表于big4 CCS18 一作是来自ETH的Petar Tsankov，通信作者是IC的Arthur Gervais

本文对以太坊的智能合约进行安全分析，满足可扩展性、完全自动化并且能够证明特定属性的安全/不安全。

安全分析分为两步：

通过符号分析合约的依赖图，从代码中精确地提取出语义信息
检查是否符合或违反模式（pattern），条件是否满足某个性质

为了实现可扩展性，所有模式都是用指定的域特定语言（DSL）规定的

目前已经代码开源，分析了18k个合约，被专家用于安全审计

INTRODUCTION

合约的广泛应用需要强安全保证，然而设计没有安全漏洞合约非常具有挑战性。

每几个月都有安全漏洞+每个漏洞都很贵

关键的挑战：

合约编程语言的图灵完备性，导致自动验证任意属性是不可判定的。现有解决方法依赖于相对通用的测试和符号执行的方法Oyente和Mythril，存在以下缺陷，导致用户需要检查所有报告中的误报并且担心漏报
- 由于欠近似，可能错过重要的违反行为
- 由于对域上特定元素不精确的建模，假阳率
- 对现实智能合约的代码覆盖率不高，Oyente只有20%

实际上，许多智能合约的安全属性本质上很难直接进行推理。解决这些挑战的可行途径是针对重要的领域特定属性构建一个自动验证器，目前的工作有仅针对重入漏洞的

本文重要的一个观察结果是可以从数据流图来检查是否符合或违反模式，原因是现实世界中漏洞倾向于违反许多简单的性质，采用pattern而不是property是因为pattern实质上更适合自动推理

本文的技术思想是定义两类模式反映给定的安全性质：

符合模式：即表示符合性质
违反模式

现有符号执行的工具存在的问题：

不报告确定性的违反模式（合并了警告和违反），需要用户手动进行分类，实验结果显示用户手动工作量减少了65.9%
现有的分析工具无法报告不安全的行为，用户需要手动检查未覆盖的代码

符号执行的方法对数字性质支持更好（溢出），本方案对审计更复杂合约的支持更好

主要贡献：

提出了一种在Datalog中对以太坊合约的依赖关系图进行符号编码的反编译器。
提出了一组合规和违规的安全模式，捕捉足够的条件来证明和反驳实际安全属性。
给出了一种端到端的实现，完全自动化合约的分析
对现有以太坊智能合约进行了广泛评估，证明了Securify可以有效地证明合约的正确性并发现违规行为。

MOTIVATING EXAMPLES

2 examples 200 millions worth of USD IN 2017

Stealing Ether

存在的安全问题：对安全非常重要的变量 owner是所有用户来说都是可写的，应该进行限制

然而由于address的空间过大，无法轻易判断是否满足该性质

Securify的检测方法是检查是否存在 owner = _owner的赋值不依赖于caller 指令(返回交易发送者的地址)

具体实现思路是通过分析合约的依赖推断数据控制流图依赖，在这里，Securify推断赋值owner = _owner不依赖于caller指令，这意味着任何用户都可以访问该赋值。一些符号检查工具执行了对相似性质的不精确检查，导致假阳率和假阴率

Frozen Funds

攻击：以太坊的智能合约可以用特定的kill指令移除区块链，如果攻击者移除 walletLibrary，存储的资金将被冻结

安全问题：允许用户存储以太币，但不保证能够取出，因为取回函数依赖于外部库，可以从以下两方面检查是否存在这个问题：

用户能够存储以太币
合约没有非零数量以太币转移的指令

Securify检查两个条件的连接，首先检查是否有stop指令，执行不依赖于转移的以太币为0。假设该stop指令对一些交易是可达的，表明用户可以用正数个ether到达，即存储以太币。其次检查是否对于所有的call指令，从合约中提取的ether数量为0

THE SECURIFY SYSTEM

以判断owner为例，介绍整体流程

绿色的输入：包括合约的字节码和定义的pattern（采用Domain-Specific Language，DSL编写），输入同样可以是solidity编写的合约

反编译EVM字节码

首先转换成无栈的静态单指令(static-single assignment form, SSA)的形式

识别函数，比如ABI_9DA8 对应的函数为initOwner

执行部分求值来解析内存和存储偏移量、跳转目的地，这些对于精确地静态分析代码都很重要

推断语义事实

分析合约推断出数据和控制流依赖

Securify推导语义事实的方式是通过层次化 Datalog（一种语言）声明式指定的，并且完全自动化，使用现有的可扩展引擎。

声明式方法的关键优势是：

（i）推理规则简洁地捕捉了对不同组件（例如合约存储）的抽象推理

（ii）更多的事实和推理规则可以轻松地添加

（iii）推理规则以模块化的方式指定（例如，内存分析独立于合约存储分析）

检查安全模式

获得所有语义事实后，SECURIFY检查符合模式和违反模式的集合。所有模式由DSL编写，方便安全专家进行扩展。DSL 是对 Securify 推导的语义事实的逻辑公式片段。其存储偏移量（表示为X）和执行这个指令的标签L都不依赖于任何可能执行合约的调用者指令的结果，则违规模式匹配。否定由 ¬ 表示，合取由 ∧ 表示

SECURIFY的输出

对于违规模式的匹配，SECURIFY能够输出导致该模式的指令所在行，如果有源码的话可以对应到solidity的行。对于没有匹配到的性质，将会给出warning

局限性

当前版本无法分析出数值性质，比如整数溢出
无法支持可达性，假设所有指令都是可达的
并不是所有的违规模式都会被攻击者利用

SEMANTIC FACTS

本节中，介绍 Securify 使用的控制流和数据流依赖关系的自动推导。在这个过程中推导出的事实被称为语义事实，并且后来用于检查安全属性。首先介绍理解此分析所必需的背景：EVM 指令集和分层 Datalog。然后介绍Securify推导的语义事实和声明式推理规则，这些规则在分层 Datalog 中指定，用于推导这些语义事实。

Backgroud

EVM

EVM指令集支持若干操作码，SECURIFY处理了所有的操作码并给出精简后的相关性较高的指令，包括：

算术运算符和比较 add
密码学哈希函数 sha3
环境信息 balance
区块信息 number timestamp
内存和存储操作 mload mstore load/store data from the memory/contract storage
系统操作如call
控制流指令如 goto

分层的Datalog

声明式逻辑语言，编写事实（谓词）和规则来推断事实。

Facts and Inference Rules

Securify首先提取了一组基本事实，这些事实对于每个指令都是成立的。这些基本事实构成了Datalog程序的输入，用于推导合约的其他事实。我们使用术语“语义事实”来指代由Datalog程序推导出的事实。在Datalog程序中，合约中出现的所有程序元素，包括指令标签、变量、字段、字符串和整数常量，都被表示为常量。

SECURITY PATTERNS

Videos

[x] CCS 2018 (1) Securify: Practical Security Analysis of Smart Contracts - YouTube
[ ] SURI 2018 (1) Securify: Practical Security Analysis of Smart Contracts | Petar Tsankov - YouTube

关键性质是在调用指令后不执行状态的改变，然而智能合约是图灵完备的，无法判定，作者观察出了危险调用和安全调用满足的一些简单的性质

工具当时可以在线访问，现在已经down了 www.securify.ch

发表会议时已经有了1k+的订阅许多专家使用

总体思路

从EVM字节码出发

Experiment on Smartbugs

根据github smartbugs/smartbugs: SmartBugs: A Framework to Analyze Ethereum Smart Contracts (github.com)的installation在虚拟机上安装docker

配置完用户组重启才能生效

采用securify对samples目录下的10个.sol文件进行分析，2线程 4g内存限制每个任务最长分析时间为60s，github给出的实验命令是600s，考虑到虚拟机是2core 4g ram，实际测试设置为60s

1	$./smartbugs -t securify -f samples/*.sol --processes 2 --mem-limit 4g --timeout 600

实验结果存储在./results/securify目录下

目录每个.sol文件分析后包括两个文件，以EtherLotto.sol为例具体来看。

smartbugs.json具体为调用工具时参数的情况

//smartbugs.json
{
    "docker": {
        "command": null,
        "detach": true,
        "entrypoint": "'/sb/bin/do_solidity.sh' '/sb/EtherLotto.sol' '/sb/bin'",
        "image": "smartbugs/security:usolc",
        "mem_limit": "4g",
        "user": 0,
        "volumes": {
            "/tmp/tmp86tp_iz9": {
                "bind": "/sb",
                "mode": "rw"
            }
        }
    },
    "filename": "samples/EtherLotto.sol",
    "platform": {
        "cpu": "12th Gen Intel(R) Core(TM) i5-12500H",
        "python": "3.10.6.final.0 (64 bit)",
        "release": "5.19.0-45-generic",
        "smartbugs": "2.0.7",
        "system": "Linux",
        "version": "#46~22.04.1-Ubuntu SMP PREEMPT_DYNAMIC Wed Jun 7 15:06:04 UTC 20"
    },
    "result": {
        "duration": 17.345403909683228,
        "exit_code": 0,
        "logs": null,
        "output": "result.tar",
        "start": 1689647289.9699748
    },
    "runid": "20230718_0228",
    "solc": "0.4.26",
    "tool": {
        "bin": "scripts",
        "command": null,
        "cpu_quota": null,
        "entrypoint": "'$BIN/do_solidity.sh' '$FILENAME' '$BIN'",
        "id": "securify",
        "image": "smartbugs/security:usolc",
        "info": "Securify uses formal verification, also relying on static analysis checks. Securify's analysis consists of two steps. First, it symbolically analyzes the contract's dependency graph to extract precise semantic information from the code. Then, it checks compliance and violation patterns that capture sufficient conditions for proving if a property holds or not.",
        "mem_limit": null,
        "mode": "solidity",
        "name": "Securify",
        "origin": "https://github.com/eth-sri/securify",
        "output": "/results/",
        "parser": "parser.py",
        "solc": true,
        "version": null
    }
}

另一个文件是result.tar，解压后可以发现

live.json文件，具体内容为模式的定义
results.json文件，给出了匹配的结果，包括violation 和 warning safe 和 conflicts

//live.json
{
  "decompiled": true,
  "finished": true,
  "patternResults": {
    "DAO": {
      "completed": true,
      "hasViolations": false,
      "hasWarnings": false,
      "hasSafe": false,
      "hasConflicts": false,
      "violations": [],
      "warnings": [],
      "safe": [],
      "conflicts": []
    },
    "DAOConstantGas": {
      "completed": true,
      "hasViolations": true,
      "hasWarnings": false,
      "hasSafe": false,
      "hasConflicts": false,
      "violations": [
        226,
        271
      ],
      "warnings": [],
      "safe": [],
      "conflicts": []
    },
    "MissingInputValidation": {
      "completed": true,
      "hasViolations": false,
      "hasWarnings": false,
      "hasSafe": true,
      "hasConflicts": false,
      "violations": [],
      "warnings": [],
      "safe": [
        116,
        116,
        111,
        116,
        111,
        130
      ],
      "conflicts": []
    },
    "TODAmount": {
      "completed": true,
      "hasViolations": true,
      "hasWarnings": false,
      "hasSafe": true,
      "hasConflicts": false,
      "violations": [
        271
      ],
      "warnings": [],
      "safe": [
        226
      ],
      "conflicts": []
    },
    "TODReceiver": {
      "completed": true,
      "hasViolations": false,
      "hasWarnings": false,
      "hasSafe": true,
      "hasConflicts": false,
      "violations": [],
      "warnings": [],
      "safe": [
        226,
        271
      ],
      "conflicts": []
    },
    "TODTransfer": {
      "completed": true,
      "hasViolations": false,
      "hasWarnings": false,
      "hasSafe": true,
      "hasConflicts": false,
      "violations": [],
      "warnings": [],
      "safe": [
        226,
        271
      ],
      "conflicts": []
    },
    "UnhandledException": {
      "completed": true,
      "hasViolations": false,
      "hasWarnings": false,
      "hasSafe": true,
      "hasConflicts": false,
      "violations": [],
      "warnings": [],
      "safe": [
        226,
        271
      ],
      "conflicts": []
    },
    "UnrestrictedEtherFlow": {
      "completed": true,
      "hasViolations": true,
      "hasWarnings": true,
      "hasSafe": false,
      "hasConflicts": false,
      "violations": [
        226
      ],
      "warnings": [
        271
      ],
      "safe": [],
      "conflicts": []
    }
  }
}

//results.json
{
  "/sb/EtherLotto.sol:EtherLotto": {
    "results": {
      "TODReceiver": {
        "violations": [],
        "warnings": [
          48,
          51
        ],
        "safe": [],
        "conflicts": []
      },
      "UnhandledException": {
        "violations": [],
        "warnings": [
          48,
          51
        ],
        "safe": [],
        "conflicts": []
      },
      "TODTransfer": {
        "violations": [],
        "warnings": [
          48,
          51
        ],
        "safe": [],
        "conflicts": []
      },
      "DAO": {
        "violations": [],
        "warnings": [],
        "safe": [],
        "conflicts": []
      },
      "TODAmount": {
        "violations": [
          51
        ],
        "warnings": [
          48
        ],
        "safe": [],
        "conflicts": []
      },
      "MissingInputValidation": {
        "violations": [],
        "warnings": [
          20,
          23,
          32
        ],
        "safe": [],
        "conflicts": []
      },
      "DAOConstantGas": {
        "violations": [
          48,
          51
        ],
        "warnings": [],
        "safe": [],
        "conflicts": []
      },
      "UnrestrictedEtherFlow": {
        "violations": [
          48
        ],
        "warnings": [],
        "safe": [
          51
        ],
        "conflicts": []
      }
    }
  }
}

根据实验结果，可能是运行的分析时间较短，许多合约分析结果为空（比如Mytoken.sol)