4、约束求解器基础：SMT求解器简介、Z3安装与基本使用、变量与约束建模
好，咱们进入第四章。说实话，很多人在符号执行这条路上卡住，不是因为控制流混淆有多难，而是倒在了约束求解器这个门槛上。我当年第一次接触SMT求解器时，也觉得这东西像个黑魔法——输入一堆逻辑公式，它就能告诉你有没有解？
嗯，其实没那么玄乎。今天我就带你把它拆开看看。
4.1 SMT求解器到底是什么？
SMT，全称是Satisfiability Modulo Theories。翻译成人话就是：在特定理论下的可满足性判定。
你想想看，传统的SAT求解器只能处理布尔变量，比如A是true还是false。但我们在逆向分析时遇到的变量，往往是整数、数组、位向量这些复杂类型。SMT求解器就是SAT的升级版——它不仅能处理布尔逻辑，还能处理算术、位运算、数组等理论。
我个人习惯把SMT求解器理解成一个「超级方程求解器」。你给它一组约束条件，它告诉你：
- SAT（可满足）：存在一组赋值让所有条件成立，并给出具体值
- UNSAT（不可满足）：不存在这样的赋值，条件矛盾
我在项目中遇到过最典型的场景：分析一个被ollvm混淆的函数，里面全是虚假控制流。手动跟踪根本走不通，但把路径条件丢给Z3，几毫秒就告诉我哪条路径是可达的。
4.2 Z3安装与基本使用
Z3是微软研究院开发的SMT求解器，目前业界用得最广。我选它不是因为微软光环，而是因为它API设计得确实顺手，Python绑定也成熟。
4.2.1 安装
安装其实就一行命令：
pip install z3-solver嗯，这里要注意。如果你在Windows上遇到什么dll缺失的问题，别慌。我曾经被这个坑过一次——后来发现是Python版本太新，Z3还没适配。建议用Python 3.8到3.11之间的版本，稳得很。
验证安装：
from z3 import *
print(version()) # 输出类似 (4, 12, 2, 0)4.2.2 第一个Z3程序
咱们写个最简单的例子，感受一下：
from z3 import *
# 创建两个整数变量
x = Int('x')
y = Int('y')
# 创建求解器
s = Solver()
# 添加约束
s.add(x + y > 5)
s.add(x - y < 3)
s.add(x > 0, y > 0)
# 求解
if s.check() == sat:
print(s.model()) # 输出一组可行解
else:
print('无解')你看，就这么简单。创建变量、添加约束、调用check()。说白了就是三步走。
s.sexpr() 查看当前约束的SMT-LIB2格式，方便排查问题。
4.3 变量与约束建模
这一节是重点。你在逆向中遇到的各种混淆，最终都要转化成约束模型。模型建得好不好，直接决定求解器能不能跑出来。
4.3.1 变量类型
Z3支持多种变量类型，我列个表给你看：
| 类型 | 构造函数 | 适用场景 |
|---|---|---|
| 整数 | Int('x') |
循环计数、数组索引 |
| 布尔 | Bool('b') |
条件分支、标志位 |
| 位向量 | BitVec('v', 32) |
寄存器值、内存地址 |
| 实数 | Real('r') |
浮点运算（较少用） |
| 数组 | Array('a', IntSort(), IntSort()) |
内存建模 |
我个人建议：在逆向分析中，优先用BitVec。为什么？因为CPU里的寄存器、内存都是固定位宽的，用BitVec最贴近真实硬件。用Int的话，Z3默认是无限精度整数，有时候会给出不符合实际的解。
4.3.2 约束建模实战
咱们来看一个真实场景。假设你在逆向中遇到这样的混淆代码：
if ((a + b) * c > 100) {
// 真实路径
} else {
// 虚假路径
}你想知道什么条件下能进入真实路径。用Z3建模：
from z3 import *
a = BitVec('a', 32)
b = BitVec('b', 32)
c = BitVec('c', 32)
s = Solver()
s.add((a + b) * c > 100)
if s.check() == sat:
print('可进入真实路径，示例值：')
m = s.model()
print(f'a = {m[a]}, b = {m[b]}, c = {m[c]}')
else:
print('路径不可达')你看，就这么几行代码，就把一个复杂的条件分支建模清楚了。
4.3.3 复杂约束：位运算与算术运算混合
混淆中最恶心的是位运算和算术运算混在一起。比如：
if ((x ^ 0xDEAD) + (y & 0xFF) << 2 == 0x12345678) { ... }建模时直接照搬表达式就行：
x = BitVec('x', 32)
y = BitVec('y', 32)
s.add((x ^ 0xDEAD) + ((y & 0xFF) << 2) == 0x12345678)Z3对位运算的支持非常好。异或、与、或、移位，它都能处理。这也是为什么它适合做逆向分析——混淆代码里全是这些东西。
4.4 知识体系总览
下面这张图是我自己梳理的本章知识结构，你看一眼就能明白整体脉络：
4.5 避坑总结
最后，我把自己踩过的坑整理一下，你记好了：
- 变量类型选错：用Int建模位运算，结果跑出超范围的值。记住，逆向分析优先用BitVec。
- 约束过于宽松：只加了一个条件，求解器给出几千种解，反而不好分析。适当收紧约束，让解空间变小。
- 忽略符号扩展：BitVec做比较时，注意符号位。Z3默认是有符号比较，如果你需要无符号，用
ULT()、UGT()这些函数。 - 求解超时：遇到复杂约束，Z3可能跑很久。我习惯设置超时：
s.set("timeout", 10000)，10秒没结果就放弃。
嗯，这一章就到这儿。约束求解器这东西，上手不难，但真正用好需要多练。你回去把上面几个例子跑一遍，感受一下Z3的「脾气」，后面学符号执行就顺了。