企业官网建设流程全解析

本篇文章围绕 Trail of Bits 的演讲《Binary analysis, meet the blockchain》（Mark Mossberg，Northsec 2018 与 High Confidence Software and Systems Conference 2018），系统讲解如何把经典的二进制分析技术——符号执行——引入以太坊智能合约审计。你将掌握 EVM 的字节码执行模型、符号执行与约束求解器的工作原理，以及用开源工具 Manticore 对合约进行自动化漏洞检测的完整实践路径。

演讲概览：两个世界的一次握手

二进制分析（Binary analysis）与区块链（Blockchain）原本分属两个领域：前者研究传统可执行程序（x86/ARM 等）的逆向与漏洞发现，后者则依赖以太坊虚拟机的去中心化执行环境。这篇演讲的主题，正是把前者的核心武器——符号执行——移植到后者的智能合约场景中。

演讲内容分三步展开：

1. 介绍以太坊及其智能合约的执行模型（EVM 字节码、账户、交易）；
2. 介绍符号执行的基本原理（路径探索、约束求解、状态空间）；
3. 讨论两者结合时面临的独特技术挑战——区块链语义、约束求解器、虚拟机内部机制，并最终落在 Manticore 这一开源实现上。

Manticore 是 Trail of Bits 开发的开源符号执行引擎，在本仓库中，它的能力由多份配套资料佐证：同主题的演讲 Automatic bugfinding for the blockchain（Ekoparty 2017）详细阐述了 Manticore 作为"支持 EVM 的动态符号执行引擎"的设计与实现；Symbolic Execution for Humans（O'Reilly Security Conference 2017）则从理论到实践介绍了符号执行的原理与 Manticore 的用法；而 Manticore - EthCC 2018 工作坊提供了完整的可运行示例代码，是本文实战部分的核心素材。

为什么是符号执行：与传统测试的差异

在深入 EVM 之前，先理解符号执行的价值。传统软件测试（包括模糊测试）每次只验证一次具体的程序执行路径；而符号执行将输入抽象为"符号值"，通过解释执行程序并在分支点收集路径约束，从而同时推理大量可能的执行路径。其系统化特性带来两个直接收益：

• 高覆盖率：只要约束可解，每条可达路径都能被探索，不再依赖人工构造的测试用例；
• 自动发现缺陷：当某条路径以异常状态（如REVERT、INVALID、溢出）结束时，求解器可以反解出触发该缺陷的具体输入。

符号执行与模糊测试互补：模糊测试擅长快速探索浅层路径，符号执行则擅长深入复杂分支条件。DARPA Cyber Grand Challenge 等赛事已经证明了符号执行在自动化漏洞挖掘中的实战价值，但对多数开发者而言它仍然陌生——这正是这篇演讲"面向人类"的科普动机。

以太坊智能合约的技术语境

EVM 与字节码执行模型

智能合约部署在以太坊上，以 EVM 字节码形式运行。EVM 是一个基于栈的虚拟机，所有操作针对 256 位字进行。对二进制分析工程师而言，EVM 更像"一个目标指令集"：

• 它是确定性、隔离的执行环境，合约之间通过消息调用交互；
• 状态由账户（账户余额、存储、代码）构成，交易触发代码执行并改变状态；
• 特殊的操作码（如SSTORE/SLOAD访问存储、CALL发起跨合约调用、REVERT/INVALID终止执行）构成了合约的安全关键面。

为什么合约需要形式化分析

Solidity 是主流的智能合约语言，但"仍然年轻"。即便是一行看似无害的算术，也可能在 256 位运算下溢出；msg.sender的信任模型、转账与检查的顺序（check-effects-interactions）、重入攻击等，都是审计中的高频缺陷。历史上多起大型攻击事件（损失动辄数百万美元）证明：共识协议保证了执行的可信，却无法保证合约逻辑的正确性。社区审计工具仍处于"幼年期"，开发者常常忽略最基础的安全建议。

因此，面向 EVM 的符号执行不是学术炫技，而是把成熟的程序分析理论移植到"钱即代码"的场景：一次能覆盖全部可达路径的分析，恰好匹配合约"部署后不可修改"的特性——上线前的自动化深度检查，比上线后的补丁重要得多。

符号执行 × 区块链：独特的组合挑战

把符号执行用到智能合约上，并非简单地把已有引擎指向新指令集。演讲点出了三组核心挑战：

1. 区块链语义：合约的执行不孤立——它依赖调用者、消息值（msg.value）、区块状态（时间戳、区块号）和跨合约调用。符号执行必须把这些环境因素也符号化，否则会丢失大量真实路径。此外，一个合约可能被多次调用，状态在调用间持续累积，分析需要模拟"多条交易序列"而非单次调用。

2. 约束求解器：EVM 的 256 位字宽让算术约束天然复杂；SSTORE/SLOAD、CALL等操作产生与存储和跨合约状态相关的约束；路径爆炸（path explosion）让朴素探索难以收敛。引擎需要在符号化、具体化（concretization）、启发式探索之间做取舍。

3. 虚拟机内部机制：EVM 的栈模型、内存模型、gas 计量与调用深度限制，都必须被精确建模。gas 不足导致的状态回滚（revert）本身就是一条值得分析的路径——真实攻击常利用 gas 边界。

Manticore 正是针对这些挑战的实现：它模拟区块链环境（账户、存储、消息），用 SMT 求解器处理路径约束，并对 EVM 操作码逐一建模，从而支持"人工辅助 + 自动检测"的审计工作流。

实战：用 Manticore 分析智能合约

以下示例全部来自本仓库的 Manticore - EthCC 2018 工作坊（作者 Josselin Feist），可直接在 Manticore 环境中复现。

环境与基本流程

Manticore 面向 EVM 的入口是ManticoreEVM。一个完整分析流程包含四步：

1. 创建区块链模拟器（ManticoreEVM()）；
2. 创建账户与部署合约（create_account/solidity_create_contract）；
3. 用符号值调用合约函数（m.SValue）；
4. 检查终止状态并生成测试用例（generate_testcase）。

simpleRun.py 是最小的完整示例：

from manticore.ethereum import ManticoreEVM # initiate the blockchain m = ManticoreEVM() source_code = ''' pragma solidity^0.4.20; contract Simple { function f(uint a) payable public { if (a == 65) { revert(); } } } ''' # Initiate the accounts user_account = m.create_account(balance=1000) contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0) # Call f(a), with a symbolic value contract_account.f(m.SValue, user_account) print "Results are in %s" % m.workspace m.finalize() # stop the exploration

关键点解读：

• m.SValue表示符号输入。函数f(uint a)的参数a是符号值，Manticore 会同时探索a == 65（进入revert()）与a != 65（正常返回）两条路径；
• create_account(balance=1000)创建外部账户（模拟调用者），solidity_create_contract(source_code, owner=user_account, balance=0)以指定源码部署合约，owner与balance分别对应部署者与合约初始余额；
• 每次运行的结果（各路径的输入、输出、约束与测试用例）都会写入m.workspace指向的工作目录；
• m.finalize()停止探索并收尾。

检测 REVERT / INVALID：从路径约束到缺陷复现

simpleThrow.py 演示了缺陷检测的标准模式：遍历m.terminated_states，检查最后一条交易的执行结果是否为REVERT或INVALID，若是则生成测试用例：

from manticore.ethereum import ManticoreEVM m = ManticoreEVM() # initiate the blockchain source_code = ''' pragma solidity^0.4.20; contract Simple { function f(uint a) payable { if (a == 65) { throw; } } } ''' # Initiate the accounts user_account = m.create_account(balance=1000) contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0) # Call f(a), with a symbolic value contract_account.f(m.SValue, caller=user_account) # Check if an execution ends with a REVERT or INVALID for state in m.terminated_states: last_tx = state.platform.transactions[-1] if last_tx.result in ['REVERT', 'INVALID']: print "Error found in f() execution (see %s)" % m.workspace m.generate_testcase(state, 'BugFound')

在 Solidity 0.4.x 中throw编译为INVALID（0.5+ 语义为revert()的REVERT），因此检查last_tx.result属于REVERT或INVALID即可覆盖两种终止语义。m.generate_testcase(state, 'BugFound')会为该状态固化为可复现的具体输入。

还原符号输入：CONCAT 与路径约束

simpleConstraint.py 展示了如何从字节码层还原出触发缺陷的具体参数值，这对审计报告至关重要：

from manticore.ethereum import ManticoreEVM from manticore.core.smtlib import Operators from manticore.core.smtlib import solver m = ManticoreEVM() # initiate the blockchain source_code = ''' pragma solidity^0.4.20; contract Simple { function f(uint a) payable { if (a == 65) { throw; } } } ''' # Initiate the accounts user_account = m.create_account(balance=1000) contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0) # Call f(a), with a symbolic value contract_account.f(m.SValue, caller=user_account) ## Check if an execution ends with a REVERT or INVALID for state in m.terminated_states: last_tx = state.platform.transactions[-1] if last_tx.result in ['REVERT', 'INVALID']: # return the first symbolic input input0 = state.input_symbols[0] # skip the function id, and extract the 32 bytes corresponding to the first parameter input0 = Operators.CONCAT(256, *input0[4:36]) # we do not consider the path were a == 65 state.constrain(input0 != 65) if not solver.check(state.constraints): print "Error found in infeasible path" continue print "Error found in f() execution (see %s)" % m.workspace m.generate_testcase(state, 'BugFound')

这段代码的要点：

• 交易 calldata 的前 4 字节是函数选择器（function id），因此取input0[4:36]跳过它、截取第一个参数对应的 32 字节，再用Operators.CONCAT(256, *...)拼成 256 位符号表达式；
• state.constrain(input0 != 65)人为排除a == 65这条已知路径，配合solver.check(state.constraints)验证剩余路径的可行性——这正体现了符号执行中"约束即路径定义"的核心思想：你可以主动追加约束，把分析聚焦到感兴趣的路径子集；
• 如果约束不可满足（check返回 False），说明该路径不可达，输出相应提示后跳过。

综合演练：整型溢出与未保护钱包

工作坊还提供了两道练习及其参考解法，非常适合完整走一遍"发现漏洞 → 构造约束 → 反解输入"的闭环。

溢出检测。overflow.sol 是存在隐患的合约：

pragma solidity^0.4.20; contract Overflow { uint public sellerBalance=0; function add(uint value) public returns (bool){ sellerBalance += value; // complicated math, possible overflow } }

参考解法 overflow.py 展示了多交易序列分析与状态约束的组合：

from manticore.ethereum import ManticoreEVM from manticore.core.smtlib import Operators, solver m = ManticoreEVM() # initiate the blockchain source_code = '''...''' # 即上述 Overflow 合约 # Generate the accounts user_account = m.create_account(balance=1000) contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0) #First add won't overflow uint256 representation contract_account.add(m.SValue, caller=user_account) #Potential overflow contract_account.add(m.SValue, caller=user_account) contract_account.sellerBalance(caller=user_account) for state in m.running_states: # Check if input0 > sellerBalance # last_return is the data returned last_return = state.platform.last_return_data # First input (first call to add) input0 = state.input_symbols[0] # retrieve last_return and input0 in a similar format last_return = Operators.CONCAT(256, *last_return) # starts at 4 to skip function id input0 = Operators.CONCAT(256, *input0[4:36]) state.constrain(Operators.UGT(input0, last_return)) if solver.check(state.constraints): print "Overflow found! see %s"%m.workspace m.generate_testcase(state, 'OverflowFound')

分析逻辑值得细读：第一次add(m.SValue)不会溢出，第二次add(m.SValue)才可能让sellerBalance += value在 uint256 上回绕。脚本随后读取sellerBalance()的返回值（last_return_data），将第二次调用的输入值与当前余额都还原成 256 位表达式，追加约束"输入大于余额"（Operators.UGT(input0, last_return)）——这正是"加法溢出成立"的充要条件；若约束可满足，即存在让余额回绕的具体输入，Manticore 便生成测试用例。这里也示范了读取状态函数返回值并把它纳入约束分析的手法。

未保护钱包。练习文件 unprotectedWallet.sol 对应典型的权限缺陷（如withdraw未校验调用者），参考解法 unprotectedWallet.py 的思路同样是：符号化调用者/参数 → 约束出"非预期调用者却成功取款"的状态 → 反解触发输入。

此外，仓库中另一场 Devcon 4 工作坊 Using Manticore and Symbolic Execution to Find Smart Contracts Bugs - Devcon 4 提供了同主题的进阶示例 my_token.sol（一个存在溢出与余额检查缺陷的代币合约），可与本文示例相互印证。

从演讲到工具链：Manticore 在审计中的定位

这场演讲的历史意义在于：它把"符号执行 × EVM"从构想推进到了可用的开源工具，并直接服务于 Trail of Bits 的智能合约审计业务。后续发展印证了这条技术路线的生命力——Manticore 的 EVM 能力随后被用于检测交易置换攻击（Detecting Transaction Replacement Attacks with Manticore，Empire Hacking 2020），攻击者通过把自己的交易插队到合法交易之前来窃取奖励；这种攻击非常隐蔽，而符号执行可以系统性枚举交易的时序组合，把"API 是否可被置换"变成可判定的问题。

对今天的智能合约安全研究者而言，这场演讲传递的方法论依然适用：

1. 先建模，再分析：把 EVM 的栈、存储、gas 与交易环境精确建模，是任何形式化工具的基础；
2. 符号输入 + 路径约束 = 漏洞证据：漏洞不只是"被发现"，还能被反解成一组可复现的具体输入；
3. 自动化与人机协作结合：Manticore 的定位是"人工辅助的自动检测"——分析师负责制定约束与目标，引擎负责穷举路径。

进一步阅读

• 演讲幻灯片：Binary-analysis-meet-the-blockchain.pdf
• 姊妹演讲：Automatic bugfinding for the blockchain（EVM 技术细节与常见漏洞类型）
• 理论入门：Symbolic Execution for Humans
• 实战工作坊：Manticore - EthCC 2018、Manticore - Devcon 4
• 应用延伸：Detecting Transaction Replacement Attacks with Manticore