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

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

用自己熟悉的语言学习以太坊DApp开发: Java | Php | Python | .Net / C# | Golang | Node.JS | Flutter / Dart

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

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