如何使用Manticore来发现智能合约漏洞

固态智能合约安全性测试形式化验证

高级

Trailofbits

构建安全的合约

2020年1月13日

16 分钟阅读

本教程的目的是展示如何使用 Manticore 自动发现智能合约中的漏洞。

安装

Manticore 需要使用 python 3.6。它可以通过 pip 或使用 docker 来安装。

使用 docker 的 Manticore

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox

最后一个命令在一个可访问您当前目录的 docker 中运行 eth-security 工具箱。您可以更改您主机中的文件，并从 docker 中运行文件上的工具

在 docker 中，运行：

solc-select 0.5.11
cd /home/trufflecon/

使用 pip 的 Manticore

pip3 install --user manticore

建议采用 solc 0.5.11。

运行脚本

使用 python 3 运行一个 python 脚本：

python3 script.py

动态符号化执行简介

Nutshell 中的动态符号化执行

动态符号化执行(DSE)是一种程序分析技术，用于探究具有高度语义意识的状态空间。这项技术是基于 "程序路径"的发现，以一种称为path predicates的数学公式表示。就概念来说，这种技术对路径预测的操作分为两步：

它们是利用对程序输入的约束来构建的。
它们被用来生成程序输入，从而导致相关路径的执行。

这种方法不会产生误报，因为所有被识别的程序状态都可以在具体执行过程中被触发。例如，如果分析发现了一个整数溢出，就可以保证它是可重现的

路径预测示例

为了了解 DSE 如何工作，请考虑以下示例：

1f(uint a).
2
3  if (aa== 65) }
4      // bug 存在
5
6
7}
8
 复制

因为 f()包含两个路径，DSE 将构建两个不同的路径预测：

路径 1： a == 65
路径 2: Not (a == 65)

每个路径预测都是一个数学公式，可以传递给所谓的 SMT 求解器，求解器将尝试解方程式。对于路径1，求解器会说，可以用a=65探索路径。对于路径2，求解器可以给a指定一个 65 以外的任何值，例如a=0。

验证属性

Manticore 允许完全控制每个路径的所有执行情况。因此，它允许您在几乎任何东西上添加任意限制。这种控制允许在合约上创建财产。

请考虑下面的示例：

1function unsafe_add(uint a, uint b) returns(uint c)。
2  c = a + b；// no overflow protection
3  return c；
4}
5
 复制

函数中只有一个要探索的路径：

路径 1: c = a + b

使用 Manticore，您可以对溢出进行检查，并对路径预测加以限制：

c = a + b AND (c < a OR c < b)

如果有可能找到一个a和b的估值，对于这个估值，上面的路径预测是可行的，这意味着您发现了一个溢出。例如，求解器可以生成输入a = 10 , b = MAXUINT256。

如果您考虑一个固定版本：

1function safe_add(uint a, uint b) returns(uint c){
2  c = a + b;
3  require(c->=a);
4  require(c)>=b);
5  return c;
6}
7
 复制

与溢出检查相关的公式是：

c = a + b AND (c >= a) AND (c=>b) AND (c < a OR c < b)

这个公式无法得以解决；在其他领域，这是一个在safe_add中，c总会增加的证明。

因此，DSE 是一个强大的工具，可以验证您代码的任意限制。

在 Manticore 下运行

我们将看到如何探索使用 Manticore API 的智能合约。目标是以下智能合约example.sol：

1pragma solidity >=0.4.24 <0.6.0;
2
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
10
显示全部
 复制

运行一个独立的探索方式

您可以通过以下命令直接在智能合约上运行 Manticore（project可以是一个 Solidity 文件，或者是项目目录）：

$ manticore project

您将会获得像这个一样的测试案例输出（顺序可能有变）：

1...
2... m.c.manticore:INFO: Generated testcase No. 0 - STOP
3... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
4... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
5... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
6... m.c.manticore:INFO: Generated testcase No. 4 - STOP
7... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
8... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
9... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
11
显示全部

在没有额外信息的情况下，Manticore 将利用新的符号交易探索智能合约，直到它不再探索合约上的新途径为止。 Manticore 不会在失败后执行新的交易（如恢复原状后）。

Manticore 将在一个mcore_*目录中输出信息。除其他外，您将在这个目录中找到：

global.summary：覆盖面和编译器警告
test_XXXXX.summary：覆盖面、前一次的说明、每次测试案例的帐户余额
test_XXXXX.tx：每个测试案例的交易详细列表

在这里，Manticore 发现了 7 个测试案例，它们对应于（文件名顺序可能会改变）：

	交易 0	交易 1	交易 2	结果
test_00000000.tx	合约创建	f(!=65)	f(!=65)	停止
test_00000001.tx	合约创建	回退函数		撤销
test_00000002.tx	合约创建			返回
test_00000003.tx	合约创建	f(65)		撤销
test_00000004.tx	合约创建	f(!=65)		停止
test_00000005.tx	合约创建	f(!=65)	f(65)	撤销
test_00000006.tx	合约创建	f(!=65)	回退函数	撤销

检索摘要 f(!=65)表示使用不同于 65 的任何值调用的调用的 f。

正如您可以注意到的那样，Manticore 为每个成功或撤销的交易生成一个独特的测试案例。

如果您想要快速的代码检查，请使用--quick-mode标志（它禁用 bug 检测器、gas 计算...）

通过 API 操纵智能合约

本节介绍如何通过 Manticore Python API 操纵智能合约的细节。您可以使用 python 扩展名*.py创建新文件，并通过将 API 命令（下面将介绍其基础内容）添加到这个文件中来写入必要的代码，然后使用$ python3 *.py命令运行它。您也可以直接在 python 控制台中执行下面的指令，使用$python3命令来运行控制台。

创建帐户

首先，您要通过以下命令启动一个新的区块链：

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
 复制

使用 m.create_account 创建一个非合约账号：

1user_account = m.create_account(balance=1000)
2
 复制

可以使用 m.solidity_create_contract 部署一个 Solidity 合约：

1source_code = '''
2pragma solidity >=0.4.24 <0.6.0;
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
10'''
11# Initiate the contract
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
显示全部
 复制

概览

可以使用 m.create_account 和 m.solidity_create_contract 创建用户账户和合约账户。

执行交易

Manticore 支持两种类型的交易：

原始交易：已探索所有函数
命名交易：只探索一个函数

原始交易

使用 m.transaction 执行原始交易：

1m.transaction(caller=user_account,
2              address=contract_account,
3              data=data,
4              value=value)
5
 复制

调用者、地址、数据或交易的值可以是具体的或抽象的：

m.make_symbolic_value 创建一个符号值。
mmmake_symbolic_buffer(size) 创建一个符号字节数组。

例如：

1symbolic_value = m.make_symbolic_value()
2symbolic_data = m.make_symbolic_buffer(320)
3m.transaction(caller=user_account,
4              address=contract_address,
5              data=symbolic_data,
6              value=symbolic_value)
7
 复制

如果数据是象征性的，Manticore 将在交易执行期间探索合约中的所有函数。查看Hands on the Ethernaut CTF文章中的回退函数解释，对于理解函数选择的工作原理会有所帮助。

命名交易

函数可以通过其的名称执行。要使用 user_account 中的符号值以及 0 ether 执行f(uint var)，请使用：

1symbolic_var = m.make_symbolic_value()
2contract_account.f(symbolic_var, caller=user_account, value=0)
3
 复制

如果没有指定交易的value，则默认为 0。

概览

交易的参数可以是具体的或抽象的
原始交易将探索所有函数
函数可以通过其名称来调用

工作区

m.workspace目录用作所有生成的文件的输出目录：

1print("Results are in {}".format(m.workspace))
2
 复制

终止探索

要停止探索，请使用 m.finalize()。一旦这个方法被调用，就不应该再发送任何交易，而且 Manticore 会针对所探索的每一条路径生成测试案例。

总结：在 Manticore 下运行

将所有先前的步骤放在一起，我们就会得到：

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14print("Results are in {}".format(m.workspace))
15m.finalize() # stop the exploration
16
显示全部
 复制

以上所有代码都可以在example_run.py中找到。

获取投掷路径

我们现在将为路径生成特定的输入，以在f()中引发异常。目标仍为以下智能合约 example.sol。

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
9
 复制

使用状态信息

执行的每个路径都有其区块链的状态。此状态要么是准备就绪，要么是被终止了，也就是说，它达到了 THROW 或 REVERT 指令状态。

m.ready_states: 已准备就绪状态列表（他们没有执行 REVERT/INVALID）
m.killed_states：终止状态列表
m.all_states：所有状态

1for state in m.all_states:
2    # do something with state
3
 复制

您可以访问状态信息。例如：

state.platform.get_balance(account.address)：帐户余额
state.platform.transactions：交易列表
state.platform.transactions[-1].return_data：最后一笔交易返回的数据

最后一笔交易返回的数据是一个数组，可以用 ABI.deserialize 转换为一个值，例如：

1data = state.platform.transactions[0].return_data
2data = ABI.deserialize("uint", data)
3
 复制

如何生成测试案例

使用 m.generate_testcase(state, name) 生成测试案例：

1m. generate_testcase(state, 'BugFound')
2
 复制

概览

您可以使用 m.all_states 对状态进行迭代
state.platform.get_balance(account.adds)返回帐户余额
state.platform.transactions返回交易列表
transaction.return_data是返回的数据
m.generate_testcase(state, name)为状态生成输入

总结：获取抛出路径

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14## Check if an execution ends with a REVERT or INVALID
15for state in m.terminated_states:
16    last_tx = state.platform.transactions[-1]
17    if last_tx.result in ['REVERT', 'INVALID']:
18        print('Throw found {}'.format(m.workspace))
19        m.generate_testcase(state, 'ThrowFound')
20
显示全部
 复制

以上所有代码都可以在example_run.py中找到。

注意我们可以生成一个更简单的脚本，因为所有由 terminated_state 返回的状态在其结果中都有 REVERT 或 INVALID：这个例子只是为了演示如何操作 API。

添加限制

我们将看到如何对探索加以约束。我们将作出这样的假设：f()的文档指出，该函数从未在a == 65的情况下被调用，因此任何a == 65的错误都不是真正的错误。目标仍为以下智能合约example.sol：

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
9
 复制

运算符

运算符模块使约束操作变得简便，除此之外，它还提供了其他功能：

Operators.AND，
Operators.OR，
Operators.UGT（无符号大小），
Operators.UGE（无符号大于或等于），
Operators.ULT（无符号小于），
Operators.ULE（无符号小于或等于）。

请使用以下代码导入模块：

1from manticore.core.smtlib import Operators
2
 复制

Operators.CONCAT用于将一个数组与一个值级联。例如，一个交易的 return_data 需要转变为一个值，以便与另一个值进行检查对比：

1last_return = operators.CONCAT(256,*last_return)
2
 复制

约束

您可以在全局范围内或针对某个特定的状态使用约束。

全局约束

使用 m.constrain(constraint) 添加全局约束。例如，您可以从一个符号地址调用合约，并将这个地址约束为特定的值：

1symbolic_address = m.make_symbolic_value()
2m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
3m.transaction(caller=user_account,
4              address=contract_account,
5              data=m.make_symbolic_buffer(320),
6              value=0)
7
 复制

状态约束

使用 state.constrain(constraint) 为一个特定状态添加约束。该约束可用来在探索状态后对其进行约束，以检查状态上的某些属性。

检查约束

使用solver.check(state.constracts)来了解约束是否仍然可行。例如，以下代码将 symbolic_value 限定为不等于 65 ，并检查状态是否仍然可行。

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # state is feasible
4
 复制

摘要：添加限制因素

通过在前面的代码中添加约束，我们获得：

1from manticore.ethereum import ManticoreEVM
2from manticore.core.smtlib.solver import Z3Solver
3
4solver = Z3Solver.instance()
5
6m = ManticoreEVM()
7
8with open("example.sol") as f:
9    source_code = f.read()
10
11user_account = m.create_account(balance=1000)
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
14symbolic_var = m.make_symbolic_value()
15contract_account.f(symbolic_var)
16
17no_bug_found = True
18
19## Check if an execution ends with a REVERT or INVALID
20for state in m.terminated_states:
21    last_tx = state.platform.transactions[-1]
22    if last_tx.result in ['REVERT', 'INVALID']:
23        # we do not consider the path were a == 65
24        condition = symbolic_var != 65
25        if m.generate_testcase(state, name="BugFound", only_if=condition):
26            print(f'Bug found, results are in {m.workspace}')
27            no_bug_found = False
28
29if no_bug_found:
30    print(f'No bug found')
31
显示全部
 复制

以上所有代码都可以在example_run.py中找到。

上次编辑: , Invalid DateTime

编辑页面

帮助更新此页面

没有错误！

Start here

Nexus basics

Nexus protocol

如何使用Manticore来发现智能合约漏洞

安装

使用 docker 的 Manticore

使用 pip 的 Manticore

运行脚本

动态符号化执行简介

Nutshell 中的动态符号化执行

路径预测示例

验证属性

在 Manticore 下运行

运行一个独立的探索方式

通过 API 操纵智能合约

创建帐户

概览

执行交易

原始交易

命名交易

概览

工作区

终止探索

总结：在 Manticore 下运行

获取投掷路径

使用状态信息

如何生成测试案例

概览

总结：获取抛出路径

添加限制

运算符

约束

全局约束

状态约束

检查约束

摘要：添加限制因素