z3库

下载z3库

pip3 install z3-solver

基本变量类型

整型(Int)，实型(Real)和向量(BitVec)

整型

  1. Int(name, ctx=None)，创建一个整数变量，name是名字
  2. Ints (names, ctx=None)，创建多个整数变量，names是空格分隔名字

实数

  1. real(name, ctx=None)，创建一个实变量，name是名字

  2. reals (names, ctx=None)，创建多个实变量，names是空格分隔名字

  3. realVal (val, ctx=None)，创建一个实常量，有初始值，没名字。

向量

BitVec(变量名,变量的大小（单位bit）)

  1. BitVec(name,bv,ctx=None)，创建一个位向量，name是他的名字，bv表示大小

  2. BitVecs(name,bv,ctx=None)，创建一个有多变量的位向量，name是名字，bv表示大小

  3. BitVecVal(val,bv,ctx=None)，创建一个位向量，有初始值，没名字。

常用API

  1. 创建约束求解器 s = Solver()
  2. 列方程s.add(...)
  3. 判断解是否存在 （存在就打印返回sat）s.check()
  4. 求解 print(s.model()[向量名])

用起来还是挺简单的，只不过这里必须要加check()检测不然会报错，如图：

# 导入Z3约束求解库
from z3 import *

# 定义一个名为'x'的整数符号变量
x = Int('x')

# 定义一个名为'y'的整数符号变量
y = Int('y')

# 创建一个新的求解器对象，用于解决一组约束
s = Solver()

# 向求解器添加三个约束条件：
# 1. x 大于 2
# 2. y 小于 10
# 3. x 和 2倍的y 的和等于 7
s.add(x > 2, y < 10, x + 2*y == 7)

# 检查求解器中的约束是否有解
s.check()

# 如果求解器中的约束有解，则打印出满足这些约束的模型（即变量的赋值）
print(s.model())

例

import z3

s = z3.Solver()
flag = [z3.BitVec(f'flag_{i}', 8) for i in range(40)]

cipher = [
     98, 113, 163, 181, 115, 148, 166,  43,   9,  95,
    165, 146,  79, 115, 146, 233, 112, 180,  48,  79,
     65, 181, 113, 146,  46, 249,  78, 183,  79, 133,
    180, 113, 146, 148, 163,  79,  78,  48, 231,  77
]

for i in range(40):
    s.add(32 <= flag[i], flag[i] <= 126)
    s.add(flag[i] * 17 == cipher[i])

if s.check() == z3.sat:
    m = s.model()
    print(''.join(chr(m[f].as_long()) for f in flag))

# BaseCTF{yoUr_CrYpt0_1earNinG_5tarTs_n0w}