12.1 概述

用“未知数（比如代数里的x、y）”代替真实数值去“模拟运行”程序，看所有可能的分支路径会得出什么结论。

12.1.1 符号执行与正常执行的对比

想象你在玩一个解谜游戏，游戏里有很多岔路，每条岔路门口有个守卫，他会根据你手里的钥匙（输入值）决定让不让你通过。

普通执行（具体执行）：

你拿一把真的钥匙（比如 x=5, y=3）去试试，能通过就走这条路线，不通就换钥匙再试。这样要试很多次才能知道哪条路能通。

符号执行：

你不用真的钥匙，而是拿一张空白通行证，上面写着“x = α₁, y = α₂”（α₁、α₂ 可以是任何数）。

你拿着这张通行证走到岔路口，守卫说：“想要过这个 if (x >= 5) 的大门，必须 α₁ ≥ 5。”

于是你在通行证背面记下这个条件，然后继续往前走。

走到下一个路口又有新条件，你都记下来。

最后你看看背面记的所有条件，用数学方法算一算：α₁ 和 α₂ 取什么具体数值能满足所有这些条件？

一旦算出来，你就知道该打造哪把真钥匙才能走到终点。

符号执行的过程：

1. 开始符号化
   • 把 x 当作符号 α₁，y 当作符号 α₂。
   • z = x + y 就成了符号表达式：α₁ + α₂。
2. 遇到第一个分支 if (x >= 5)
   • 符号执行引擎会分两支探索，但我们先看其中一支：走 true 分支（即 x >= 5）。
   • 在这一支的“路径约束”中记录：α₁ ≥ 5。
3. 执行 foo(x, y, z)
   • 因为已经满足 α₁ ≥ 5，所以能执行到 foo。
   • 此时我们想找具体输入值，就解方程：α₁ ≥ 5。
   • 一个很简单的解是 x = 5, y = 0（y 可以任意取值，因为没有约束 y）。
4. 如果继续执行
   • 后面还会遇到 if (y < x)，又会产生新的路径约束（比如 α₂ + (α₁ + α₂) < α₁）。
   • 每一条路径都会积累一组约束条件，最终用“约束求解器”算出能走到这条路径的输入值。

12.1.2 符号执行的变体和局限

1. 静态符号执行 vs 动态符号执行

类比：

• 静态符号执行（SSE） 就像你在纸上模拟一场足球比赛，不真正踢球，只是用符号和规则推导所有可能的比赛路径。
  • ✅ 优点：可以分析你没实际运行的环境（比如在 Windows 上分析 Linux 程序）。
  • ❌ 缺点：如果比赛要和真实裁判（系统调用/内核）交互，你就得猜裁判的反应，可能猜错。
• 动态符号执行（DSE / 混合执行） 就像你实际踢一场比赛，但同时记笔记：“如果我刚才射门偏左一点会怎样？”然后下一场实际比赛中你故意偏左再试。
  • ✅ 优点：实际运行程序，外部交互（裁判、队友行为）都是真实的，不会出错。
  • ❌ 缺点：一次只能试一条路径，如果目标路径和当前路径差别很大，你要反复踢很多场才能走到那里。

2. 在线 vs 离线符号执行

类比：

• 在线符号执行：像你有超能力，在每一个选择点（比如游戏里的岔路）分裂成两个自己，同时走两条路继续探索。
  • 好处：不用走回头路，效率高。
  • 坏处：内存消耗大（分身越多，记忆负担越大）。
• 离线符号执行：像你只有一个身体，先走一条路到底，然后读档回到岔路口，再走另一条。
  • 好处：内存小（只记录一条路径的状态）。

3. 符号状态与内存访问问题

类比：
想象你在管理一个仓库（内存），货物（变量）放在不同货架（地址）上。

• 如果仓库管理员说“请把货物放到第 α 号货架”，而 α 可能是 1、2、3…N：
  • 完全符号内存：你会为 α 的每种可能值复制整个仓库状态（α=1 时放这儿，α=2 时放那儿…），但若 α 可能值很多，状态会爆炸。
  • 地址具体化：你强行假设 α 是某个固定值（比如 α=1），这样简单，但可能漏掉 α=2 时才会触发的 bug。

这就像你考试做选择题，如果题目说“选 A 或 B 或 C 都可能”，符号执行要模拟三种情况，而具体化就是直接假定选 A 继续做题。

4. 路径覆盖与启发式方法

类比：
你要探索一个巨大的迷宫（程序），分支多得数不清（路径爆炸）。

• 深度优先搜索（DFS）：一条路走到黑，直到死胡同才回头。适合找深层漏洞。
• 广度优先搜索（BFS）：每次只走一步，但平行推进所有路径。能更快覆盖浅层分支。

如果迷宫有循环（比如绕圈的走廊），你可能永远走不完——这就是符号执行遇到无限循环时的局限。

5. 实际工具举例（联系已知）

• Triton / angr：像高级调试器 + 符号推理引擎，可用于二进制分析。
• KLEE：直接在程序中间表示（LLVM IR）上做符号执行，类似在“汇编之上的一层通用语言”上分析。
• S2E：基于虚拟机，能符号执行整个系统（包括内核），就像用模拟器运行整个操作系统并观察符号化输入的影响。

12.2 使用Z3进行约束求解

12.2.1 证明指令的可达性

x = int(argv[0])
y = int(argv[1])
z = x + y
if(x >= 5)
foo(x, y, z)
y = y + z
if(y < x)
baz(x, y, z) ← 我们想知道输入什么 x、y 能执行到这里
else
qux(x, y, z)
else
bar(x, y, z)


你可以把这个问题想象成一个密室逃脱游戏：

• 目标房间：baz 函数。
• 密码锁：每个 if 语句就是一个密码锁，需要满足条件（比如 x ≥ 5）才能通过。
• 你：符号执行引擎。
• Z3：一个超级密码破解器，你告诉它所有锁的密码条件，它帮你算出一组能开所有锁的数字（x 和 y）。

步骤分解：

1. 列出所有密码条件（路径约束）
   要到 baz，必须通过以下关卡：
   • 第一关：if(x >= 5) ✅ 走 then 分支 → 条件：x ≥ 5
   • 第二关：if(y < x) ✅ 走 then 分支 → 条件：y₂ < x
     （注意：此时 y 已经变成 y₂ = y + z，而 z = x + y）
2. 避免变量重复赋值的混淆（SSA）
   就像你玩游戏时，y 的值会变化：
   • 初始 y（从输入来）我们叫 y₁。
   • 执行 y = y + z 后，新的 y 我们叫 y₂。
     这样在列方程时就不会出现“y = 3 且 y = 5”的矛盾。
3. 把条件翻译成 Z3 能懂的语言（SMT-LIB）
   • 声明变量：(declare-const x Int)
   • 添加等式和不等式：
     • z = x + y₁ → (assert (= z (+ x y₁)))
     • x ≥ 5 → (assert (>= x 5))
     • y₂ = y₁ + z → (assert (= y₂ (+ y₁ z)))
     • y₂ < x → (assert (< y₂ x))
4. 询问密码破解器（Z3）
   • (check-sat) → 如果返回 sat（可满足），说明存在这样的 x、y。
   • (get-model) → 返回一组具体值（比如 x=5, y₁=-1, z=4, y₂=3）。
5. 验证
   代入 x=5, y=-1：
   • z = 5 + (-1) = 4
   • x≥5 ✅
   • y₂ = -1 + 4 = 3
   • y₂ < x → 3 < 5 ✅
     所以执行 baz(5, 3, 4) 是可达的！

使用z3如下：

除了Int 之外，Z3 还支持其他常见的数据类型，如 Real（用于浮点数）和
Bool，以及更复杂的类型，如Array。

z3.exe -in
(declare-const x Int)     声明变量xyz
(declare-const y Int)
(declare-const z Int)
(declare-const y2 Int)
(assert (= z (+ x y)))     使用assert命令添加约束公式
(assert (>= x 5))     添加x>=5的断言
(assert (= y2 (+ y z)))
(assert (< y2 x))
(check-sat)     check-sat命令检查断言栈的可满足性
sat  意味着断言系统是可满足的，表明在模拟的程序路径上baz是可达的
(get-model)  向Z3 查询一个模型，：一个满足所有断言的所有常量的具体赋值。
(
(define-fun y () Int  定义了一个名为y的函数，该函数不接收任何参数并返回−1的Int值。这意味着在此模型中，常量y的值为−1。
(- 1))
(define-fun y2 () Int
3)
(define-fun z () Int
4)
(define-fun x () Int
5)
)      Z3求解x=5、y=−1、z=4

12.2.2 证明指令的不可达性

这次添加了x和y必须非负的约束条件

$
z3 -in
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const y2 Int)
(assert (>= x 0))
(assert (>= y 0))
(assert (= z (+ x y)))
(assert (>= x 5))
(assert (= y2 (+ y z)))
(assert (< y2 x))
(check-sat)
unsat   不可达

12.2.3 证明公式的永真性

永真性（validity）就像数学中的恒等式，比如 (a+b)² = a² + 2ab + b²，无论 a、b 取什么值都成立。

永真公式：在任何情况下都为真的逻辑表达式。

可满足性（sat）就像方程有解，比如 x + 2 = 5 有解 x=3，但不是对所有 x 都成立。

证明方法：要证明一个公式永真，可以证明它的否定公式是不可满足的（无解）。意思是反面无解。

双向引理指出((p→q)∧(r→s)∧(pv¬s)) (qv¬r)

• 如果以下三个条件同时成立：
  1. 如果 p 为真则 q 为真
  2. 如果 r 为真则 s 为真
  3. p 为真或者 s 为假（至少一个成立）
• 那么一定能推出：
  • q 为真或者 r 为假（至少一个成立）

这看起来复杂，但 Z3 可以帮我们验证这是否永远成立。

正面证明：

(declare-const p Bool)
(declare-const q Bool)
(declare-const r Bool)
(declare-const s Bool)
(assert (=> (and (and (=> p q) (=> r s)) (or p (not s)))(or q (not r))))
(check-sat)
sat
(get-model)
(
(define-fun p () Bool
false)
(define-fun q () Bool
false)
(define-fun s () Bool
false)
(define-fun r () Bool
false)
)

这只能证明存在某些 p、q、r、s 的值使公式成立。就像验证 x > 0 时发现 x=1 成立，但不能证明对所有 x 都成立。

反面证明：

(declare-const p Bool)
(declare-const q Bool)
(declare-const r Bool)
(declare-const s Bool)
(assert (not (=> (and (and (=> p q) (=> r s)) (or p (not s))) (or q (not r)))))
(check-sat)
unsat

12.2.4 简化表达式

declare-const x Int)
(declare-const y Int)
(simplify (+ (* 3 x) (* 2 y) 5 x y))    原始：3x + 2y + 5 + x + y
(+ 5 (* 4 x) (* 3 y))  被z3简化了：5 + 4x + 3y

12.2.5 使用位向量对机器码建立约束模型

核心问题：为什么二进制程序分析不能用普通整数？

已知：

• 我们学过整数在数学上是无限的精度（可以任意大）
• CPU 的寄存器是固定的位数（例如 x86 的寄存器是 32 位或 64 位）

未知：

• 在二进制程序中，整数运算实际上发生在固定宽度的容器内
• 例如加法 0xFFFFFFFF + 1 在 32 位寄存器中会溢出成 0

位向量与普通整数的区别

• 普通整数 (Int) ≈ Python 的 int（可以无限大）
• 位向量 (BitVec) ≈ C 语言的 int32_t（最多到 2³¹-1），可以回绕为0.

为什么二进制分析需要用位向量？

已知类比 👉 假设你要分析一个二进制程序中的指令：

现实情况：

1. eax 是 32 位的寄存器
2. 如果加法结果超出了 2³²-1（比如 0xFFFFFFFF + 1）
3. 在实际的 CPU 上，结果会变成 0（自动回绕）

符号执行（symbolic execution）必须准确模拟这种 wrap-around 行为，
特别是当程序涉及整数溢出漏洞时。

位向量的基本语法

假设我们现在要创建两个 32 位的位向量 x 和 y，以及对应的运算：

基础声明

基本运算

假设我们要计算 z = x + y：

用位向量模拟汇编指令

假设我们要建模指令：

这在 Z3 中可以写成：

12.2.6 用位向量求解不透明谓词

不透明谓词的定义：

• 一个看起来像正常 if 条件的分支判断
• 但实际上结果永远是固定的（要么永远为真，要么永远为假）
• 逆向工程师很难一眼看出这个规律

if (x + x*x % 2 != 0) { // 这个条件实际上永远为假 // 这里是死代码，永远不会执行

confusing_fake_code(); }

Z3 如何自动化验证这个不透明谓词？

我们要验证的命题：“不存在任何 x 使得 (x + x²) % 2 ≠ 0“

换成 Z3 的语言就是：

; 声明一个 64 位的整数 x（对应 x86-64 的寄存器）
(declare-const x (_ BitVec 64))

; 断言：存在 x 使得 (x + x*x) % 2 ≠ 0
(assert (not (= (bvsmod (bvadd (bvmul x x) x) (_ bv2 64)) (_ bv0 64))))

; 检查这个断言是否可满足
(check-sat) ; 返回 unsat

• (bvmul x x) = x * x（位向量乘法）
• (bvadd ... x) = (x*x) + x
• (bvsmod ... (_ bv2 64)) = 对 2 取模（有符号模运算）
• (_ bv2 64) = 数值为 2 的 64 位向量

12.4 练习

x = int(argv[0])
y = int(argv[1])
z = x*x
w = y*y
if(z <= 1)
if( ((z + w) % 7 == 0) && (x % 7 != 0) )
foo(z, w)
else
if((2**z – 1) % z != 0)
bar(x, y, z)
else
z
= z + w
baz(z, y, x)
z = z*z
qux(x, y, z)

1.

初始状态: x=X, y=Y, z=X², w=Y²
│
├── 路径1: z <= 1 (X² ≤ 1)
│ ├── 路径1.1: (X²+Y²)%7=0 ∧ X%7≠0
│ │ ├── 执行: foo(X², Y²)
│ │ └── 最终: z = (X²)², 执行 qux(X, Y, X⁴)
│ │
│ └── 路径1.2: ¬((X²+Y²)%7=0 ∧ X%7≠0)
│ └── 最终: z = (X²)², 执行 qux(X, Y, X⁴)
│
└── 路径2: z > 1 (X² > 1)
├── 路径2.1: (2^X² - 1)%X² ≠ 0
│ ├── 执行: bar(X, Y, X²)
│ └── 最终: z = (X²)², 执行 qux(X, Y, X⁴)
│
└── 路径2.2: (2^X² - 1)%X² = 0
├── z = X² + Y²
├── 执行: baz(X²+Y², Y, X)
└── 最终: z = (X²+Y²)², 执行 qux(X, Y, (X²+Y²)²)

2.1 问题分析：证明可达性

foo可达：当 z <= 1 且 (z+w)%7==0 且 x%7!=0

bar可达：当 z > 1 且 (2^z - 1) % z != 0

baz可达：当 z > 1

2.2 Z3 建模方案

由于涉及幂运算 2^z（可能很大），我们需要选择合适的位向量宽度。考虑到实际程序中的整数范围，我选择 32位 位向量。

; 声明符号变量（32位位向量）
(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))

; 定义中间变量
(define-const z (_ BitVec 32) (bvmul x x)) ; z = x*x
(define-const w (_ BitVec 32) (bvmul y y)) ; w = y*y

; 检查是否存在 x,y 使得 foo 可达
; 条件: z <= 1 AND (z+w)%7==0 AND x%7 != 0

(push) ; 保存当前状态

; 断言 foo 的条件
(assert (bvsle z (_ bv1 32))) ; z <= 1
(assert (= (bvurem (bvadd z w) (_ bv7 32)) (_ bv0 32))) ; (z+w)%7 == 0
(assert (not (= (bvurem x (_ bv7 32)) (_ bv0 32)))) ; x%7 != 0

; 检查可满足性
(check-sat)
sat
(get-model)
(
(define-fun y () (_ BitVec 32)
#x5b810171)
(define-fun x () (_ BitVec 32)
#x01e03084)
(define-fun w () (_ BitVec 32)
(bvmul y y))
(define-fun z () (_ BitVec 32)
(bvmul x x))
)

(pop) ; 恢复状态

检查 bar 的可达性

; 检查 bar 的可达性
; 条件: z > 1 AND (2^z - 1) % z != 0

(push)

; z > 1 (注意：bvsgt 是有符号比较)
(assert (bvsgt z (_ bv1 32)))

; 计算 2^z - 1 （由于 z 可能很大，需要小心处理）
; 使用 Z3 的幂函数：
(define-fun pow2 ((n (_ BitVec 32))) (_ BitVec 32)
(ite (= n (_ bv0 32)) (_ bv1 32)
(bvshl (_ bv1 32) n))) ; 实际上应该是 1 << n，但需要处理 n >= 32 的情况

; 更安全的方法：使用 bvshl，但要确保 z 在合理范围内
(assert (bvult z (_ bv32 32))) ; 限制 z < 32 以避免溢出

(define-const two_power_z (_ BitVec 32) 
(bvshl (_ bv1 32) z)) ; 2^z

(define-const two_power_z_minus_1 (_ BitVec 32)
(bvsub two_power_z (_ bv1 32))) ; 2^z - 1

; (2^z - 1) % z != 0
(assert (not (= (bvurem two_power_z_minus_1 z) (_ bv0 32))))

(check-sat)
(get-model)

(pop)

检查 baz 的可达性

; 检查 baz 的可达性 
; 条件: z > 1 AND (2^z - 1) % z == 0

(push)

(assert (bvsgt z (_ bv1 32)))
(assert (bvult z (_ bv32 32))) ; 限制 z < 32

(define-const two_power_z (_ BitVec 32) 
(bvshl (_ bv1 32) z))

(define-const two_power_z_minus_1 (_ BitVec 32)
(bvsub two_power_z (_ bv1 32)))

; (2^z - 1) % z == 0
(assert (= (bvurem two_power_z_minus_1 z) (_ bv0 32)))

(check-sat)
(get-model)

(pop)

完整脚本

; 完整验证三个函数的可达性
(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))

(define-const z (_ BitVec 32) (bvmul x x))
(define-const w (_ BitVec 32) (bvmul y y))

(echo "=== 检查 foo 可达性 ===")
(push)
(assert (bvsle z (_ bv1 32)))
(assert (= (bvurem (bvadd z w) (_ bv7 32)) (_ bv0 32)))
(assert (not (= (bvurem x (_ bv7 32)) (_ bv0 32))))
(check-sat)
(get-model)
(pop)

(echo "=== 检查 bar 可达性 ===")
(push) 
(assert (bvsgt z (_ bv1 32)))
(assert (bvult z (_ bv32 32))) ; 避免位移溢出
(define-const two_power_z (_ BitVec 32) (bvshl (_ bv1 32) z))
(define-const two_power_z_minus_1 (_ BitVec 32) (bvsub two_power_z (_ bv1 32)))
(assert (not (= (bvurem two_power_z_minus_1 z) (_ bv0 32))))
(check-sat)
(get-model)
(pop)

(echo "=== 检查 baz 可达性 ===")
(push)
(assert (bvsgt z (_ bv1 32)))
(assert (bvult z (_ bv32 32)))
(define-const two_power_z (_ BitVec 32) (bvshl (_ bv1 32) z)) 
(define-const two_power_z_minus_1 (_ BitVec 32) (bvsub two_power_z (_ bv1 32)))
(assert (= (bvurem two_power_z_minus_1 z) (_ bv0 32)))
(check-sat)
(get-model)
(pop)

3. 查找不透明谓词

3.1 代码中的分支条件分析

回顾代码中的条件判断：

1. 条件A: if(z <= 1)，其中 z = x²
2. 条件B: if( ((z + w) % 7 == 0) && (x % 7 != 0) )，其中 z = x², w = y²
3. 条件C: if((2**z - 1) % z != 0)，其中 z = x²

3.2 检查条件A: x² <= 1

; 检查是否存在 x 使得 x² > 1（验证条件A是否可能为假）
(declare-const x (_ BitVec 32))

(define-const z (_ BitVec 32) (bvmul x x))

; 检查条件A的否定是否可满足（即是否存在 x 使得条件A为假）
(assert (bvsgt z (_ bv1 32))) ; x² > 1

(check-sat)
; 如果 sat → 条件A不是不透明谓词
; 如果 unsat → 条件A恒真

3.3 检查条件B: (x² + y²) % 7 == 0 ∧ x % 7 ≠ 0

(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))

(define-const z (_ BitVec 32) (bvmul x x))
(define-const w (_ BitVec 32) (bvmul y y))

; 检查是否存在 x,y 使条件B为真
(assert (= (bvurem (bvadd z w) (_ bv7 32)) (_ bv0 32))) ; (x²+y²)%7=0
(assert (not (= (bvurem x (_ bv7 32)) (_ bv0 32)))) ; x%7≠0

(check-sat)

 3.3 检查条件C: (2^x² - 1) % x² ≠ 0

; 检查是否存在 x 使条件C为假（即 (2^x² - 1) % x² = 0）
(declare-const x (_ BitVec 32))

(define-const z (_ BitVec 32) (bvmul x x))

; 限制 x² < 32 避免位移溢出
(assert (bvult z (_ bv32 32)))
(assert (bvsgt z (_ bv1 32))) ; 只关心 z>1 的情况

(define-const two_power_z (_ BitVec 32) (bvshl (_ bv1 32) z))
(define-const two_power_z_minus_1 (_ BitVec 32) (bvsub two_power_z (_ bv1 32)))

; 寻找使条件C为假的 x（即 (2^z-1)%z = 0）
(assert (= (bvurem two_power_z_minus_1 z) (_ bv0 32)))

(check-sat)
(get-model)

3.4 完整的不透明谓词检查脚本

(echo "=== 检查条件A (x²<=1) 是否为不透明谓词 ===")
(declare-const x1 (_ BitVec 32))
(define-const z1 (_ BitVec 32) (bvmul x1 x1))
(assert (bvsgt z1 (_ bv1 32))) ; 检查是否存在 x 使 x²>1
(check-sat)
; sat → 不是不透明谓词

(echo "=== 检查条件B ((x²+y²)%7=0 ∧ x%7≠0) 是否为不透明谓词 ===")
(declare-const x2 (_ BitVec 32))
(declare-const y2 (_ BitVec 32))
(define-const z2 (_ BitVec 32) (bvmul x2 x2))
(define-const w2 (_ BitVec 32) (bvmul y2 y2))
(assert (and (= (bvurem (bvadd z2 w2) (_ bv7 32)) (_ bv0 32))
(not (= (bvurem x2 (_ bv7 32)) (_ bv0 32)))))
(check-sat)
; sat → 不是不透明谓词

(echo "=== 检查条件C ((2^x²-1)%x²≠0) 是否为不透明谓词 ===")
(declare-const x3 (_ BitVec 32))
(define-const z3 (_ BitVec 32) (bvmul x3 x3))
(assert (and (bvsgt z3 (_ bv1 32)) (bvult z3 (_ bv32 32))))
(define-const two_power_z3 (_ BitVec 32) (bvshl (_ bv1 32) z3))
(define-const expr (_ BitVec 32) (bvurem (bvsub two_power_z3 (_ bv1 32)) z3))

; 检查条件C是否恒真（即其否定是否不可满足）
(assert (= expr (_ bv0 32))) ; 条件C的否定：寻找使它为假的 x
(check-sat)
(get-model)
; 如果 sat → 存在 x 使条件C为假 → 条件C不是恒真
; 如果 unsat → 条件C恒真 → 是不透明谓词