re-Z3约束求解器

从moectf2026Mewtype题目了解Z3约束求解器在逆向题目中使用

z3-solver介绍

python库，可以用来“解方程”，给出约束条件，能让其给出符合约束的结果。相当于爆破求值

安装

1	pip install z3-solver

需要额外注意：这个pip命令会安装工具到这个版本中

如果在后续编译过程中报错说没有安装z3，考虑是没用上同一版本的python解释器

比如vscode，按ctrl+shift+p后搜索这个则可更换

基本语法

代码开头

引入z3库（注意我们创建的文件不要命名为z3）

from z3 import *

创建变量

比如说我们知道了flag的长度为54，可以使用列表推导式批量创建

s = [BitVec(f's{i}',32)for i in range(54)]

一般在解CTF题目的时候我们要用BitVec

需注意：大小写一定要符合规范，比如And，Or要按照他的规则写

编写约束条件

在定义完变量之后，编写约束条件之前

先写一个

solver111 = Solver()

然后写n个

total = BitVecVal(0, 32)和solver111.add()

前者的作用是创建一个初始值为0，填充32位的变量

把条件丢进去add后的()里即可

输出结果

1
2
3

if solver.check() == sat:
    print(solver.model())
else:

以上四步是最基本的语法，下面通过moectf2026的Mewtype这道题目的Z3代码来进阶理解

拆脚本理解

from z3 import *

s = [BitVec(f's{i}',32)for i in range(54)]
# Define the problem
solver = Solver()

prefix = "moectf{"
for i, ch in enumerate(prefix):
    solver.add(s[i] == ord(ch))
solver.add(s[53] == ord('}'))


total = BitVecVal(0, 32)
for v in s:
    total += v
solver.add(total == 5138)

xoresult = BitVecVal(0, 32)
for v in s:
    xoresult ^=v
solver.add(xoresult == 26)

squri = BitVecVal(0, 32)
for v in s:
    squri += v*v
solver.add(squri == 520600)

lrj_sum = BitVecVal(0, 32)
for v in range(53):
    lrj_sum += s[v] * s[v+1]
solver.add(lrj_sum == 467644)


targets = (
        10111, 11290, 137705, 13834, 12017, 882822, 2861, 6952, 148686,
        9290, 9962, 153274, 13069, 9595, 871218, 9834, 10851, 1584472,
        9149, 5765, 159511, 9289, 5093, 126222, 11887, 4921, 152566,
        13114, 6109, 140607, 13366, 9447, 156018, 9712, 11045, 1795540,
        15852, 4864, 1389923, 10278, 5369, 1586542, 10519, 5995,
        1281695, 4298, 5674, 963368, 10232, 5085, 880083, 10095, 15119
    )
for i in range(53):
    a = s[i]
    b = s[i + 1]
    c = s[(i + 17) % 54]
    target = targets[i] ^ 90
    mode = i % 3
    if mode == 0:
        solver.add(a + b + c * c == target)
    elif mode == 1:
        solver.add(a * b + c == target)
    else:
        solver.add(a * a + b * b + c * c * c == target)

for v in s:
    solver.add(v >= 32 , v <= 126)


if solver.check() == sat:
    m = solver.model()
    result = ''.join(chr(m[v].as_long()) for v in s)
    print(result)
else:
    print("No solution found")

乍眼一看很唬人

看看新增的部分

已知flag格式

prefix = "moectf{"
for i, ch in enumerate(prefix):
    solver.add(s[i] == ord(ch))
solver.add(s[53] == ord('}'))

这里是因为我们已经知道了flag格式，加一个约束条件来减少时间

先定义了一个字符串，然后对这个字符串用for循环方式对它进行遍历，然后约束使每一位相等

取出字符串

if solver.check() == sat:
    m = solver.model()
    result = ''.join(chr(m[v].as_long()) for v in s)
    print(result)
else:
    print("No solution found")

里面是什么意思？

for v in s：按顺序遍历 54 个变量
m[v]：从模型里取出变量 v 的值。返回的是一个 Z3 的数值对象。
.as_long()：把 Z3 数值对象转成 Python 整数。
chr(...)：把整数转成对应的 ASCII 字符。
chr(109) → 'm'。
''.join(...)：把 54 个字符拼接成一个完整的字符串。
最终 result 就是 flag，例如 moectf{...}。

为什么不能直接 print(solver.model())?

solver.model() 返回的是一个 Z3 的模型对象，它不是一个字符串。直接打印它会输出类似这样的东西：
1
[s0 = 109, s1 = 111, s2 = 101, s3 = 99, s4 = 116, s5 = 102, s6 = 123, ...]
这是每个变量（s0、s1、…）被赋的具体整数值。
它有几个问题：

不是连续的字符：你看到的是变量名和数字，而不是 moectf{...} 这样的字符串。

顺序不保证：Z3 模型内部可能不按 s0, s1, s2... 的顺序排列，直接打印可能乱序。

包含额外信息：模型里可能还有其他临时变量，直接打印会混杂在一起。

需要手动转换：数字 109 要转成字符 'm'，必须用 chr()。

所以，必须遍历 s 列表，按顺序从模型里取值、转字符、拼接。

https://chat.deepseek.com/share/bfkmkp2ge3gz70owd1

附

枚举多解的写法（编辑于261016）

while (solver.check() == sat):
	model1 = solver.model()
    print("找到一个解：")
    sol1 = [model1[s[i]].as_long() for i in range(N)]
    print(''.join([chr(c) for c in sol1]))    
    solver.add(Or([s[i] != model1[s[i]] for i in range(N)]))

z3 ctf/re z3约束求解器