3、约束求解器入门：Z3安装与基本使用，求解简单算术约束

好，咱们进入第三个环节。前面聊了符号执行的基本概念，你可能会想：“这东西听起来挺牛，但具体怎么把约束条件解出来？”

嗯，这就得靠约束求解器了。我个人习惯把约束求解器比作“数学题的自动答题机”。你给它一堆条件，它告诉你有没有解，有解的话解是什么。

今天咱们就上手最主流的求解器——Z3。我会带着你从安装开始，一步步写出第一个能跑起来的求解脚本。

3.1 为什么是Z3？

市面上约束求解器不少，比如STP、Boolector、CVC4。但我为什么推荐Z3？

说白了，Z3是微软研究院的产物，社区活跃，文档齐全。我在做漏洞挖掘项目时，遇到复杂的位运算约束，Z3基本都能搞定。其他求解器有时候会卡住，Z3的表现相对稳定。

另外，Z3支持Python接口。这对我们做安全分析的人来说太友好了。你想想看，Python写原型多快啊。

3.2 安装Z3

安装过程其实很简单。我建议直接用pip安装，省心。

pip install z3-solver

如果你在Linux下，也可以从源码编译。但我个人觉得没必要折腾，pip版本足够用了。

小提示： 如果你在Windows上遇到安装失败，多半是Python版本问题。建议用Python 3.8以上版本。我曾经在Python 3.6上踩过坑，换了版本就好了。

安装完成后，验证一下：

python -c "from z3 import *; print('Z3 installed successfully')"

看到成功提示，就说明环境搭好了。

3.3 第一个Z3程序：解一个简单方程

咱们从最基础的开始。假设有个方程：x + 2 = 5。求x。

用Z3怎么写？看代码：

from z3 import *

# 创建一个变量x，类型是整数
x = Int('x')

# 创建求解器对象
s = Solver()

# 添加约束条件
s.add(x + 2 == 5)

# 检查是否有解
if s.check() == sat:
    print("有解，解为：", s.model())
else:
    print("无解")

运行结果：

有解，解为： [x = 3]

嗯，很直观对吧？

这里有几个关键点：

  • Int('x') 声明了一个整数变量。Z3支持多种类型，后面会讲。
  • Solver() 创建求解器实例。你可以把它理解成一个“问题容器”。
  • s.add() 添加约束。注意，这里用的是 ==，不是 =。因为Z3里 == 表示“等于”约束，而 = 是Python的赋值。
  • s.check() 返回 sat（可满足）或 unsat（不可满足）。
  • s.model() 给出具体的解。
注意： 初学者最容易犯的错误是把 s.add(x + 2 == 5) 写成 s.add(x + 2 = 5)。Python里单等号是赋值，双等号才是比较。Z3的约束必须用双等号。

3.4 多变量与多约束

实际漏洞挖掘中，约束条件往往不止一个。咱们来看个例子：

from z3 import *

x = Int('x')
y = Int('y')

s = Solver()

s.add(x + y == 10)
s.add(x - y == 2)

if s.check() == sat:
    print("解：", s.model())
else:
    print("无解")

输出：

解： [y = 4, x = 6]

你看，Z3自动解出了这个二元一次方程组。x=6, y=4。

我在做符号执行时，经常需要同时处理几十个约束。Z3都能应付。但要注意，约束越多，求解时间可能越长。这是NP难问题，没办法。

3.5 布尔变量与逻辑约束

除了整数，Z3还支持布尔变量。这在处理程序中的条件分支时特别有用。

from z3 import *

p = Bool('p')
q = Bool('q')

s = Solver()

s.add(Or(p, q))      # p 或 q 为真
s.add(Not(And(p, q))) # p 和 q 不能同时为真

if s.check() == sat:
    print("解：", s.model())
else:
    print("无解")

输出：

解： [q = True, p = False]

或者也可能是 p=True, q=False。Z3会给出一个可行的解。

3.6 位向量：处理底层数据

做二进制安全，免不了要处理位运算。Z3的位向量（BitVec）就是干这个的。

from z3 import *

# 声明一个8位的位向量变量
a = BitVec('a', 8)
b = BitVec('b', 8)

s = Solver()

s.add(a & b == 0x0F)   # 按位与
s.add(a | b == 0xAB)   # 按位或

if s.check() == sat:
    print("解：", s.model())
else:
    print("无解")

位向量的好处是，你可以精确控制变量的位宽。比如8位、16位、32位、64位。这在模拟CPU寄存器时非常有用。

核心概念： 位向量是连接高级语言和底层硬件的桥梁。在漏洞挖掘中，很多整数溢出、符号扩展等问题，用位向量建模最准确。

3.7 常见问题与避坑指南

我刚开始用Z3时，也踩过不少坑。这里分享几个：

  • 类型不匹配： 整数和位向量不能直接混用。比如 Int('x') + BitVec('y', 32) 会报错。需要做类型转换。
  • 求解超时： 有些约束可能让Z3陷入长时间计算。我建议设置超时：s.set("timeout", 10000)（单位毫秒）。
  • 模型不唯一： Z3只返回一个解。如果你需要所有解，需要手动添加排除约束，循环求解。
避坑指南： 我曾经在分析一个缓冲区溢出漏洞时，用整数类型建模，结果Z3给出了一个看似合理的解，但实际利用时却失败了。后来换成位向量，才找到真正的原因。所以，处理内存地址、指针运算时，务必用位向量。

3.8 实战：求解一个简单的算术约束

咱们来一个稍微综合点的例子。假设程序中有这样一段逻辑：

if (a + b > 100 && a - b < 50) {
    // 漏洞触发点
}

我们想知道，什么样的a和b能进入这个分支。

from z3 import *

a = Int('a')
b = Int('b')

s = Solver()

s.add(a + b > 100)
s.add(a - b < 50)

if s.check() == sat:
    print("满足条件的a, b：", s.model())
else:
    print("不可达")

输出：

满足条件的a, b： [b = 0, a = 101]

你看，Z3告诉我们，当a=101, b=0时，条件成立。这就是符号执行的威力——不需要实际运行程序，就能找到触发特定路径的输入。

3.9 小结

今天咱们完成了Z3的入门。从安装到第一个求解脚本，再到多变量、布尔逻辑、位向量。这些基础操作，是后续做漏洞挖掘的基石。

下一节，我会带你深入Z3的高级用法，比如数组、量词、优化求解。这些东西在分析复杂漏洞时特别有用。

嗯，今天就到这里。建议你打开电脑，把上面的代码都跑一遍。亲手试试，比看十遍都管用。

← 上一章 📖 返回目录 下一章 →