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

Solidity

智能合同

安全性。

测试

形式化验证

高级

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-toolbox。你可以从主机更改文件，并在 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

动态符号执行简介

动态符号执行简述

动态符号执行 (DSE) 是一种程序分析技术，可利用高度的语义感知来探索状态空间。这项技术基于对“程序路径”的发现，这些路径表示为称为路径谓词的数学公式。从概念上讲，此技术分两步对路径谓词进行操作：

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

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

路径谓词示例

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

1function f(uint a){
2
3  if (a == 65) {
4      // 存在一个漏洞
5  }
6
7}

由于 f() 包含两条路径，DSE 将构建两个不同的路径谓词：

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

每个路径谓词都是一个数学公式，可以将其提供给所谓的 SMT 求解器opens in a new tab，求解器会尝试求解该方程式。对于“路径 1”，求解器会指出可以使用 a = 65 探索该路径。对于“路径 2”，求解器可以为 a 指定一个 65 以外的任何值，例如 a = 0。

验证属性

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

请考虑下面的示例：

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // 没有溢出保护
3  return c;
4}

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

路径 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}

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

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

这个公式无法求解；换句话说，这证明了在 safe_add 中，c 的值总是会增加。

因此，DSE 是一个强大的工具，可以验证你代码中的任意约束。

在 Manticore 下运行

我们将了解如何使用 Manticore 应用程序接口来探索智能合约。目标是以下智能合约 example.solopens in a new tab：

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}
显示全部

运行独立探索

你可以通过以下命令直接在智能合约上运行 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...
显示全部

在没有额外信息的情况下，Manticore 将利用新的符号交易探索合约，直到它不再探索合约上的新路径为止。 Manticore 不会在失败后（例如：回滚后）执行新的交易。

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

global.summary：覆盖率和编译器警告
test_XXXXX.summary：每个测试用例的覆盖率、最后一条指令、账户余额
test_XXXXX.tx：每个测试用例的交易详细列表

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

	交易 0	交易 1	交易 2	结果
test_00000000.tx	合约创建	f(!=65)	f(!=65)	STOP
test_00000001.tx	合约创建	回退函数		REVERT
test_00000002.tx	合约创建			RETURN
test_00000003.tx	合约创建	f(65)		REVERT
test_00000004.tx	合约创建	f(!=65)		STOP
test_00000005.tx	合约创建	f(!=65)	f(65)	REVERT
test_00000006.tx	合约创建	f(!=65)	回退函数	REVERT

探索摘要 f(!=65) 表示 f 是以任何非 65 的值调用的。

正如你可以注意到的那样，Manticore 为每个成功或回滚的交易生成一个独特的测试用例。

如果你想要快速的代码探索，请使用 --quick-mode 标志（它会禁用漏洞检测器、燃料计算...）

通过应用程序接口操纵智能合约

本节详细介绍如何通过 Manticore Python 应用程序接口操纵智能合约。你可以创建扩展名为 *.py 的新 Python 文件，通过将应用程序接口命令（下文会介绍其基础知识）添加到此文件中来编写必要的代码，然后使用 $ python3 *.py 命令运行它。你也可以直接在 python 控制台中执行下面的命令，使用 $ python3 命令来运行控制台。

创建账户

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

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

使用 m.create_accountopens in a new tab 创建一个非合约账户：

1user_account = m.create_account(balance=1000)

可以使用 m.solidity_create_contractopens in a new tab 部署 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# 初始化合约
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
显示全部

总结

你可以使用 m.create_accountopens in a new tab 和 m.solidity_create_contractopens in a new tab 来创建用户账户和合约账户。

执行交易

Manticore 支持两种类型的交易：

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

原始交易

使用 m.transactionopens in a new tab 执行原始交易：

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

交易的调用者、地址、数据或值，既可以是具体的，也可以是符号的：

m.make_symbolic_valueopens in a new tab 创建一个符号值。
m.make_symbolic_buffer(size)opens in a new tab 创建一个符号字节数组。

例如：

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)

如果数据是符号的，Manticore 将在交易执行期间探索合约的所有函数。查看“Ethernaut CTF 实战”opens in a new tab文章中的回退函数解释，对于理解函数选择的工作原理会有所帮助。

命名交易

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

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

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

总结

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

工作区

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

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

终止探索

使用 m.finalize()opens in a new tab 停止探索。一旦这个方法被调用，就不应该再发送任何交易，而且 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() # 停止探索
显示全部

以上所有代码都可以在 example_run.pyopens in a new tab 中找到

获取抛出路径

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

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}

使用状态信息

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

m.ready_statesopens in a new tab：准备就绪（它们没有执行 REVERT/INVALID）的状态列表
m.killed_statesopens in a new tab：已终止状态的列表
m.all_statesopens in a new tab：所有状态

1for state in m.all_states:
2    # 对状态执行某些操作

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

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)

如何生成测试用例

使用 m.generate_testcase(state, name)opens in a new tab 生成测试用例：

1m.generate_testcase(state, 'BugFound')

总结

你可以使用 m.all_states 迭代状态
state.platform.get_balance(account.address) 返回账户的余额
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## 检查执行是否以 REVERT 或 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')
显示全部

以上所有代码都可以在 example_run.pyopens in a new tab 中找到

请注意，我们本可以生成一个更简单的脚本，因为 terminated_state 返回的所有状态在其结果中都有 REVERT 或 INVALID：本示例仅用于演示如何操纵应用程序接口。

添加约束

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

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}

操作符

Operatorsopens in a new tab 模块有助于操纵约束，它提供了以下操作符：

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

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

1from manticore.core.smtlib import Operators

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

1last_return = Operators.CONCAT(256, *last_return)

约束

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

全局约束

使用 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)

状态约束

使用 state.constrain(constraint)opens in a new tab 为特定状态添加约束。它可用于在探索状态后对其进行约束，以检查状态上的某些属性。

检查约束

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

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # 状态可行

总结：添加约束

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

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## 检查执行是否以 REVERT 或 INVALID 结束
20for state in m.terminated_states:
21    last_tx = state.platform.transactions[-1]
22    if last_tx.result in ['REVERT', 'INVALID']:
23        # 我们不考虑 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')
显示全部

以上所有代码都可以在 example_run.pyopens in a new tab 中找到

页面最后更新： 2024年4月26日

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

安装

通过 docker 使用 Manticore

通过 pip 使用 Manticore

运行脚本

动态符号执行简介

动态符号执行简述

路径谓词示例

验证属性

在 Manticore 下运行

运行独立探索

通过应用程序接口操纵智能合约

创建账户

总结

执行交易

原始交易

命名交易

总结

工作区

终止探索

总结：在 Manticore 下运行

获取抛出路径

使用状态信息

如何生成测试用例

总结

总结：获取抛出路径

添加约束

操作符

约束

全局约束

状态约束

检查约束

总结：添加约束

本教程对你有帮助吗？