Mythril符号执行原理【Solidity安全】

发表于 | 分类于

Mythril是一个基于符号执行技术的以太坊智能合约安全工具， 其预置的检测模块可以发现合约中存在的一些安全问题，例如 整数溢出和重入漏洞。本文的目的是学习理解Mythril的符号执行机制， 以便开发自己的Solidity安全分析模块。

Mythril的设计目标之一是让安全分析工具更简单易用。换句话说 就是你不需要是计算机科学领域的博士就可以从符号化分析中获益。

1、符号执行概述

为了说明Mythril的运行机制，我们需要先了解Mythril使用的核心技术 —— 符号执行（Symbolic Execution）。如果你之前已经比较了解符号 执行的一般思路，那么本文有助于帮助你梳理相关的概念。

我认为解释符号执行的最简单的方法是真正执行它并画图展示出 执行过程中发生的事情。为此，我们将使用下面的solidity函数 作为我们分析的目标，让我们看看是否可以使用符号化分析来得出 函数的结果为10。

2、具体执行： Concrete Execution

在我们开始符号执行之前，先看看具体执行的结果。我们可以用多个不同的 输入来执行函数execute(uint256)。例如对于输入4，将产生如下的执行过程：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Initial state (function entry): 
- currently executing: line 1 
- input = 4 
step1: 
- currently executing: line 2 
- input = 4 
- result = uninitialized 
step2: 
- currently executing: line 3 
- input = 4 
- result = 0 
step3: 
- currently executing: line 6: 
- input = 4 
- result = 0

上述过程的图形化表示如下：

我们可以尝试不同的输入，直到找出可以让函数返回10的输入， 这种方法被称为模糊测试（Fuzzing）。

3、符号执行：Symbolic Execution

最后我们要符号化执行程序了。这意味着我们不再将具体的输入（例如4） 带入程序执行，而是用一个符号来指代具体的输入。将该符号称为x， x可以是任何有效的uint256值。现在让我们再次执行程序。

前两步的执行简单直白，容易理解：

现在开始进入有趣的部分。在第3行输入与10进行比较，但是输入是x， 它可以是任何具体的值，因此，x > 10和 x < 10都是可能的。如果 这种情况发生，我们可以创建两个新的状态分支，其中一个对应 x > 10， 另一个对应x <= 10。我们还需要记录这些约束，这样就可以决定具体 的输入将执行哪个路径。

现在让我们将状态图扩展到下一步的执行：

下面是我们通过符号化执行生成的状态。有了这些符号化的状态，我们可以 写一个简单的程序来找出什么输入值可以得到输出10。

1
2
3
4
5
6
7
8
9
10
11
12
for state in states:
  # Let's filter all the states that are not return statements
  if state.currently_executing != 6:
    continue
  # We want the result to be 10, let's formulate that as a constraint
  result_constraint = (state.result == 10)
  
  # If it is possible to satisfy both the path constraints (these are the constraints collected on each branch)
  # and the result constraint then there must be an input that makes the function return 10
  if is_possible(result_constraint and state.constraints):
    # Using SMT solving we can get an input that will satisfy all the constraints and make the function return 10
    print(give_satisfying_input(result_constraints and state.constraints))

查看上述代码的执行结果，可以清楚地了解只有状态3和状态5需要考虑。

对于状态3，函数is_possible(result_constraint and state.constraints) 将返回false，因为对于该状态我们得到result =0。

现在看一下状态5，我们发现了一些更有趣的东西。让我们看一下 这里考虑的两个约束：result == 10 and x > 10 。容易看到第一个 约束必须满足，也容易确定 x > 10可以满足，例如对于输入11。 我只是手动找了一个值来满足上述约束。再Mythril中，实际上是 利用一个SMT（Z3）求解器来找出是否可能满足这些约束条件，而且 Z3还可以给出一个可以满足约束条件的具体示例，这让我们可以 构建一个实际输入来让函数返回10。

作为函数execute分析的结论，我们可以说：

  1. 输出为10的可能性存在
  2. 可以使用输入11得到输出10

4、结语

在这篇文章中，我们介绍了如何用符号执行来分析一个简单的示例函数， 并介绍了如何编写一个简单的分析模块。在后续的文章中，我们将分析 更多更有趣的安全漏洞。

原文链接：Introduction to Mythril and Symbolic Execution

汇智网翻译整理，转载请标明出处