跳转至主要内容

如何使用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的数学公式表示。 就概念来说,这种技术对路径预测的操作分为两步:

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

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

路径预测示例

为了了解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)

如果有可能找到一个ab的估值,对于这个估值,上面的路径预测是可行的,这意味着你发现了一个溢出。 例如,求解器可以生成输入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)
显示全部
复制

概览

执行交易

Manticore支持两种类型的交易:

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

原始交易

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

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

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

例如:

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指令状态。

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日

本教程对你有帮助吗?