4、Z3求解器入门：Z3的安装、基本数据类型（Int, BitVec, Bool）、约束求解与模型获取
好，咱们正式开始玩Z3。
说实话，我第一次接触Z3的时候，心里想的是：「这玩意儿不就是个高级版的解方程工具吗？」后来真拿它去逆向一个密码学算法校验，才发现自己太天真了。Z3的强大之处在于——它不光能解方程，还能解带约束的逻辑谜题。你给它一堆条件，它告诉你「行」还是「不行」，如果行，还能给你一个具体的答案。
这一章，我们就从零开始，把Z3装好，把它的三个核心数据类型搞明白，再跑几个实际的约束求解例子。我保证，学完这一章，你就能用它去破解一些简单的密码校验了。
4.1 安装Z3：别踩我踩过的坑
安装其实很简单，但有几个细节我得提醒你。
推荐方式：pip安装
pip install z3-solver注意，包名是 z3-solver，不是 z3。我见过有人装错了包，折腾了半天。
如果你在Windows上遇到问题，大概率是Python环境变量没配好。我个人习惯用虚拟环境，干净利落。
验证安装
打开Python交互环境，输入：
from z3 import *
print(Int('x'))如果能正常输出 x，说明安装成功。
我曾经踩过的坑： 在Linux上用系统自带的Python3，结果权限不够，装不上。后来用 pip install --user z3-solver 搞定的。如果你也遇到权限问题，试试这个。
4.2 三大基本数据类型：Int、BitVec、Bool
Z3里最常用的就是这三种。说白了，它们对应着现实世界里的整数、二进制位串和真假判断。
4.2.1 Int（整数）
这个最简单，就是数学里的整数。Z3里的整数没有位数限制，可以无限大（当然，实际求解时会受内存限制）。
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()) # 输出：[x = 6, y = 4]你看，这就是一个简单的二元一次方程组。Z3一秒就解出来了。
4.2.2 BitVec（位向量）
这个才是逆向分析里的主角。为什么？因为计算机里的整数都是有位宽的——比如8位、16位、32位、64位。BitVec就是用来模拟这种固定位宽的整数。
举个例子，一个8位的BitVec，取值范围是0到255。如果你让它加1，255加1会变成0，因为溢出了。这跟真实CPU的行为一模一样。
from z3 import *
a = BitVec('a', 8) # 8位变量
b = BitVec('b', 8)
s = Solver()
s.add(a + b == 0x100) # 注意，0x100 = 256，8位装不下
if s.check() == sat:
print(s.model()) # 输出可能让你意外为什么会这样？因为8位加法，结果只保留低8位。0x100的低8位是0x00，所以实际上Z3在求解 a + b == 0。这就是溢出效应，在密码学算法里经常被利用。
核心区别：
Int：数学整数，无溢出，适合纯数学问题BitVec：固定位宽整数，有溢出，适合逆向工程和密码学
4.2.3 Bool（布尔值）
这个就是True/False。在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()) # 输出：p = True, q = False 或 p = False, q = True嗯，这里要注意：Bool变量本身不是约束，你得用逻辑运算符把它们组合起来，才能形成有意义的条件。
4.3 约束求解与模型获取
好，数据类型讲完了，咱们来聊聊核心流程。Z3求解一个问题的步骤，其实就三步：
- 声明变量：告诉Z3你要用哪些变量，什么类型
- 添加约束：把条件告诉Z3
- 求解并获取模型：让Z3干活，然后读出结果
我画了一张图，帮你理清这个流程：
你看，流程很清晰。关键就是 s.check() 返回 sat 还是 unsat。如果是 sat，就用 s.model() 把解拿出来。
4.4 实战：破解一个简单的密码校验
光说不练假把式。咱们来点实际的。
假设你逆向了一个程序，发现它有一个密码校验函数，逻辑是这样的：
def check_password(pwd):
# pwd 是一个4字节的整数
# 校验条件：
# 1. pwd 的每个字节都不为0
# 2. pwd 的低16位 + 高16位 == 0xABCD
# 3. pwd 的字节0 XOR 字节3 == 0x42
# 4. pwd 的字节1 XOR 字节2 == 0x13
return True # 如果满足所有条件用Z3来破解它：
from z3 import *
# 声明一个32位的变量
pwd = BitVec('pwd', 32)
# 提取4个字节
byte0 = Extract(7, 0, pwd) # 最低字节
byte1 = Extract(15, 8, pwd)
byte2 = Extract(23, 16, pwd)
byte3 = Extract(31, 24, pwd) # 最高字节
# 低16位和高16位
low16 = Extract(15, 0, pwd)
high16 = Extract(31, 16, pwd)
s = Solver()
# 约束1：每个字节都不为0
s.add(byte0 != 0)
s.add(byte1 != 0)
s.add(byte2 != 0)
s.add(byte3 != 0)
# 约束2：低16位 + 高16位 == 0xABCD
s.add(low16 + high16 == 0xABCD)
# 约束3：字节0 XOR 字节3 == 0x42
s.add(byte0 ^ byte3 == 0x42)
# 约束4：字节1 XOR 字节2 == 0x13
s.add(byte1 ^ byte2 == 0x13)
# 求解
if s.check() == sat:
model = s.model()
result = model[pwd].as_long()
print(f"找到密码: 0x{result:08X}")
# 输出每个字节
print(f"字节0: 0x{(result & 0xFF):02X}")
print(f"字节1: 0x{((result >> 8) & 0xFF):02X}")
print(f"字节2: 0x{((result >> 16) & 0xFF):02X}")
print(f"字节3: 0x{((result >> 24) & 0xFF):02X}")
else:
print("无解，密码校验逻辑可能有误")个人经验： 我在逆向一个嵌入式设备的固件时，遇到过类似的校验。当时用Z3几秒钟就解出来了，而手动逆向推算至少得半小时。Z3在处理这种位运算约束时，效率极高。
4.5 常见陷阱与避坑指南
用Z3的时候，有几个坑我帮你提前踩了：
陷阱1：BitVec的符号问题
BitVec默认是无符号的。如果你需要处理负数，得用 BitVecVal 或者显式转换。我曾经在解一个带符号比较的约束时，折腾了半天才发现是符号问题。
陷阱2：模型中的值怎么取出来
model[var] 返回的是Z3的内部对象，不是Python整数。你得用 .as_long() 转换。如果是Bool类型，用 .is_true() 判断。
陷阱3：约束过多导致求解变慢
Z3虽然强大，但也不是万能的。如果你加了上百个复杂的非线性约束，求解时间可能会暴涨。我的建议是：先加简单约束，逐步增加复杂度，看看Z3的反应。
4.6 小结
这一章我们搞定了三件事：
- 装好了Z3，避开了常见的安装坑
- 搞懂了Int、BitVec、Bool三种数据类型，特别是BitVec在逆向中的核心地位
- 跑通了约束求解的完整流程，并用一个实战例子演示了如何破解密码校验
说实话，Z3入门并不难，难的是怎么把实际问题转化成Z3能理解的约束。这个能力需要多练。下一章我们会深入BitVec的高级操作，比如移位、循环、符号扩展——这些都是密码学算法里经常出现的操作。
好，今天就到这里。你自己动手试试上面的例子，把密码改一改，看看Z3能不能解出来。遇到问题随时回来翻翻这一章。
公众号:蓝海资料掘金营，微信deep3321