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

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

高级

Trailofbits

构建安全的合约(opens in a new tab)

2020年1月13日

15 分钟阅读 minute read

本教程的目的是展示如何使用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}
 复制

因为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；// no overflow protection
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 API的智能合约。目标是以下智能合约example.sol(opens 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)	停止
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()
 复制

使用 m.create_account(opens in a new tab) 创建一个非合约账号：

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

可以使用 m.solidity_create_contract(opens 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# Initiate the contract
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
显示全部
 复制

概览

可以使用 m.create_account(opens in a new tab) 和 m.solidity_create_contract(opens in a new tab) 创建用户帐户和合约帐户。

执行交易

Manticore支持两种类型的交易：

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

原始交易

使用 m.transaction(opens in a new tab) 执行原始交易：

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

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

m.make_symbolic_value(opens in a new tab) 创建一个符号值。
mmmake_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将在交易执行期间探索合约中的所有函数。查看Hands on the Ethernaut CTF(opens in a new tab)文章中的回退函数解释，对于理解函数选择的工作原理会有所帮助。

命名交易

函数可以通过其的名称执行。要使用user_account中的符号值以及0 ether执行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() # stop the exploration
显示全部
 复制

以上所有代码都可以在example_run.py(opens in a new tab)中找到。

获取投掷路径

我们现在将为路径生成特定的输入，以在f()中引发异常。目标仍为以下智能合约 example.sol(opens 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_states(opens in a new tab): 已准备就绪状态列表（他们没有执行REVERT/INVALID）
m.killed_states(opens in a new tab)：终止状态列表
m.all_states(opens in a new tab)：所有状态

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

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

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.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')
显示全部
 复制

以上所有代码都可以在example_run.py(opens in a new tab)中找到。

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

添加限制

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

运算符

运算符(opens 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.constracts)来了解约束是否仍然可行。例如，以下代码将symbolic_value限定为不等于65 ，并检查状态是否仍然可行。

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

摘要：添加限制因素

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

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')
显示全部
 复制

以上所有代码都可以在example_run.py(opens in a new tab)中找到。

上次修改时间: @lukassim(opens in a new tab), 2024年4月26日

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

安装

使用docker的Manticore

使用pip的Manticore

运行脚本

动态符号化执行简介

Nutshell中的动态符号化执行

路径预测示例

验证属性

在Manticore下运行

运行一个独立的探索方式

通过API操纵智能合约

创建帐户

概览

执行交易

原始交易

命名交易

概览

工作区

终止探索

总结：在Manticore下运行

获取投掷路径

使用状态信息

如何生成测试案例

概览

总结：获取抛出路径

添加限制

运算符

约束

全局约束

状态约束

检查约束

摘要：添加限制因素

本教程对你有帮助吗？