跳转至主要内容

帮助更新此页面

🌏

本页面有新版本,但现在只有英文版。请帮助我们翻译最新版本。

翻译页面
查看英文

没有错误!🐛

此页面未翻译,因此特意以英文显示。

如何使用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 工具箱。 您可以更改您主机中的文件,并从 docker 中运行文件上的工具

在 docker 中,运行:

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 如何工作,请考虑以下示例:

1function f(uint a){
2
3 if (a == 65) {
4 // A bug is present
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)

如果有可能找到一个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}
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 为每个成功或撤销的交易生成一个独特的测试案例。

如果您想要快速的代码检查,请使用--Quickmode标志(它禁用 bug 检测器、gas 计算...)

通过 API 操纵智能合约

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

创建帐户

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

1from manticore.ethereum importer MantocoreEVM
2
3m = MantocoreEVM()
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
显示全部
📋 复制

概览

执行交易

Manticore 支持两种类型的交易:

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

原始交易

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

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

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

例如

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

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.constraint(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
编辑页面

本页面对您有帮助吗?

网站最后更新: 2022年11月25日

使用以太坊

  • 查找钱包
  • 获取 ETH
  • 去中心化应用 (dapps)
  • 第二层
  • 运行一个节点
  • 稳定币
  • 质押以太币

生态系统

  • 社区中心
  • 以太坊基金会
  • 以太坊基金会博客
  • 生态系统支持方案
  • 以太坊漏洞悬赏计划
  • 生态系统资助计划
  • 以太坊品牌资产
  • Devcon