符号执行：让代码自己说出所有秘密

各位同学，今天我们来聊聊符号执行。说实话，我第一次接触这个概念时，觉得它像魔法一样神奇。你想想看，让程序自己告诉你「我所有可能的执行路径」，这难道不酷吗？

我在审计一个DeFi协议时，就靠符号执行挖到过一个隐藏极深的漏洞。那个漏洞在普通测试中根本不会触发，但符号执行帮我找到了它。嗯，这就是我们今天要讲的核心。

符号执行原理：把具体值换成「符号」

传统测试是什么样的？你给程序一个具体输入，比如 amount = 100，然后看它怎么跑。这叫「具体执行」。

符号执行不一样。它把输入变成「符号」——比如 amount = α，α 可以代表任何值。然后程序带着这个符号一路跑下去，遇到分支就分叉，最终形成一棵「执行树」。

举个例子，看这段简单的Solidity代码：

function check(uint x) public pure returns (uint) {
    if (x > 10) {
        return x + 1;
    } else {
        return x - 1;
    }
}

具体执行时，你只能测 x=5 或 x=20 等有限情况。符号执行呢？它把 x 设为符号 α，然后发现两条路径：

• 路径1：α > 10，返回 α + 1
• 路径2：α ≤ 10，返回 α - 1

你看，一次执行就覆盖了所有可能。这就是符号执行的威力。

路径约束：每条路都有自己的「通行证」

符号执行过程中，每遇到一个分支条件，引擎就会记录下这个条件。这些条件的集合，就叫「路径约束」（Path Constraints）。

说白了，路径约束就是一条执行路径的「通行证」。只有满足这些条件，程序才会走这条路。

我习惯把路径约束想象成「路标」。比如上面那个例子：

• 走 return x + 1 这条路，路标是 α > 10
• 走 return x - 1 这条路，路标是 α ≤ 10

更复杂的合约会有更多分支，路径约束也会越来越长。我曾经分析过一个借贷协议，它的路径约束嵌套了七八层条件，看得我眼花缭乱。但正是这些约束，帮我找到了一个「只有特定条件下才会触发」的重入漏洞。

符号执行引擎：Manticore 和 hevm

工欲善其事，必先利其器。目前主流的符号执行引擎有两个：Manticore 和 hevm。我两个都用过，各有千秋。

Manticore：全功能但有点重

Manticore 是 Trail of Bits 开发的，支持EVM字节码分析。它不仅能做符号执行，还能做动态符号执行（concolic testing）。

我记得第一次用 Manticore 分析一个ERC20合约，它帮我找到了一个「转账金额溢出」的漏洞。当时我手动审计了两天都没发现，Manticore 跑了10分钟就找到了。

基本用法：

# 安装
pip install manticore

# 分析合约
from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()
# 加载合约，设置符号输入
# 然后 m.run() 开始探索

Manticore 的优点是功能全面，缺点是速度慢。遇到复杂合约，它可能会跑很久。我建议你用它做「深度分析」，而不是「快速扫描」。

hevm：轻量级但够用

hevm 是 dapphub 开发的，专门针对Solidity合约。它更轻量，速度更快，适合日常使用。

我曾经在一个项目中，用 hevm 做CI流水线的自动化测试。每次提交代码，hevm 自动跑一遍符号执行，检查是否有新的路径被引入。效果非常好。

基本用法：

# 安装
nix-env -i hevm

# 分析合约
hevm symbolic --code $(cat contract.bin) --abi $(cat contract.abi)

hevm 的优点是快，缺点是功能不如 Manticore 丰富。如果你只是做常规的路径探索和漏洞检测，hevm 完全够用。

特性	Manticore	hevm
开发团队	Trail of Bits	dapphub
执行速度	较慢	较快
功能丰富度	高（支持动态符号执行）	中（专注符号执行）
适用场景	深度审计、复杂合约	日常测试、CI集成
学习曲线	较陡	平缓

实际案例：用符号执行找「整数溢出」

光说不练假把式。我们来看一个真实案例。

假设有这样一个合约：

function transfer(address to, uint amount) public {
    require(balances[msg.sender] >= amount);
    balances[msg.sender] -= amount;
    balances[to] += amount;
}

看起来没问题？但如果你用符号执行去跑，引擎会发现：当 amount 非常大时，balances[to] += amount 可能溢出。具体来说：

• 路径约束：balances[msg.sender] ≥ amount
• 同时：balances[to] + amount > 2^256 - 1

这两个条件同时满足时，就会触发溢出。符号执行引擎会自动生成一个具体的测试用例，比如 amount = 2^256 - balances[to]，让你可以直接复现漏洞。

避坑指南：我踩过的几个坑

最后，分享几个我亲身踩过的坑：

• 路径爆炸：我曾经分析一个包含循环的合约，符号执行跑了整整一天都没结束。后来我手动限制了循环次数，才搞定。记住，符号执行对循环敏感，必要时加个「最大迭代次数」。
• 假阳性：符号执行有时会报告「不可能触发的漏洞」。比如路径约束本身就不满足，但引擎没检测到。我习惯用SMT求解器再验证一遍。
• 环境依赖：合约的运行时环境（比如block.timestamp）也会影响路径。我建议你把环境变量也符号化，避免遗漏。

好了，符号执行的内容就讲到这里。下一章我们会聊「抽象解释」——另一种形式化验证的利器。到时候见。