Z3约束求解总结

用来解决方程问题

用来解决方程问题是它最简单的用法之一

from z3 import *
 
s = Solver()
 
# Define variables
x = Real('x')
 
# Define operations (an equation in this case)
y = 6*x**2 + 11*x - 35
 
# Define constraints
s.add(y == 0)
# s.add(6*x**2 + 11*x - 35 == 0)  # Also works
 
if s.check() == sat:  # If satisfiable
    print(s.model())  # [x = 5/3]

z3默认只求一个解,如果要求多解,那么我们要修改一下代码

while s.check() == sat:  # While satisfiable
    m = s.model()
    print(m)  # [x = 5/3], [x = -7/2]
    s.add(x != m[x])  # Exclude this solution

这里的m是比较难理解的,可以把他看成一个集合,通过键值进行配对,例如这个样子

m = {
	x: ...
}

一些在CTF中的组合用法

# 目标flag是20个长度字符串
flag = [BitVec(f"flag_{i}", 8) for i in range(20)]
 
# 限制每一个字符为可打印字符
for character in flag:
    s.add(character >= 0x20, character < 0x7e)
 
# 寻找所有的可能性,并打印
while s.check() == sat:
    m = s.model()
    result = bytes([m[flag[i]].as_long() for i in range(len(flag))])
    print(result)
 
    s.add(Or([flag[i] != m[flag[i]] for i in range(len(flag))]))

flag = [BitVec(f"flag_{i}", 8) for i in range(20)]

这样的语句非常常见,经常用来初始化一个未知的数组.

for character in flag:
    s.add(character >= 0x20, character < 0x7e)

这里是将数组中的每一个8位的向量进行约束,从而满足一些条件
假设z3找到了一个解,那么m的结构大概是这样的

m = {
    flag[0]: 0x43,  # 'C'
    flag[1]: 0x54,  # 'T'
    flag[2]: 0x46,  # 'F'
    ...
}

所以接下来我们要处理这些数据,把他变成我们想要的字符串

result = bytes([m[flag[i]].as_long() for i in range(len(flag))])
print(result)

为了求出所有的可能,我们要接着再添加一些条件

s.add(Or([flag[i] != m[flag[i]] for i in range(len(flag))]))

1. m[flag[i]]

   • m 是当前 Z3 模型（s.model()），存储了变量 flag[i] 的解。
   • m[flag[i]] 获取 flag[i] 在当前解中的具体值（Z3 表达式）。

2. flag[i] != m[flag[i]]

   • 这是一个约束条件，表示“flag[i] 的新解不能等于当前解的值”。
   • 例如，若当前解中 flag[0] = 0x41（'A'），则此条件要求 flag[0] 下次不能是 0x41。

3. 列表推导式 [... for i in range(20)]

   • 对 flag 的 20 个字符分别生成 != 约束，得到一个包含 20 个条件的列表。
   • 例如：[flag[0] != 0x41, flag[1] != 0x42, ..., flag[19] != 0x7e]。

4. Or(...)

   • 将 20 个 != 条件用逻辑或（Or）连接，表示“至少有一个字符的值与当前解不同”。
   • 这是为了避免全盘否定当前解（否则可能无解），而是允许部分变化。

5. s.add(...)

   • 将 Or 条件添加到求解器 s 中，作为新的约束。
   • 下次调用 s.check() 时，Z3 会排除当前解，寻找满足新约束的解。

通过z3约束求解来解决CTF问题

陇剑杯Prover