Z3约束求解器

starts

一直不会用z3，但是爆破里面经常会需要z3来一把梭，主要是在类型转换时里面经常有个a开头的类型搞我，给我整寄了。直到现在从normal题再一次做起又碰到z3的时候想起来还是需要学习一下，这次找到了一篇比较详细的讲解。

Z3约束求解器

安装z3模块

1	pip install z3-solver

在使用z3时，开头需要这样一行

1	from z3 import *

设置变量

一般来使用z3大多数都会有位运算，所以一般就不用管Real（实数）和Int（整数），直接把变量设置成向量型就可以。

# 声明单个 16 位的变量
x = BitVec('x',16)
# 声明多个 16 位的变量
y,z = BitVecs('y z',16)

然后我们在z3里一般都会使用很多变量，需要快速添加变量。

添加 50 个 16 位 BitVec 变量 s ：

1
2

s=[BitVec ('s%d' % i,16) for i in range(50)] #声明一个列表，数据类型是向量，向量的大小是16位
flag = [BitVec('%d' % i, 8) for i in range(36)] #声名一个列表，数据类型是向量，大小是8位

创建约束求解器

1	s = Solver()

添加约束条件

以行为单位添加方程等式样子的约束条件：

1
2
3

s.add(x**2+y**2==74)
s.add(x**5-y==z)
# [y = -7, x = 5, z = 3132]

这里注意，z3不允许列表与列表之间添加==约束条件，会报错。

判断是否有解

if s.check() == sat:  #检查是否有解
    print("solver")
else:
    print("no solver")

求解并输出

1 2	ans = s.model() #求解 print(ans)

TIP

一般来说经常会使用z3来爆破，求解flag时需要将变量约束在可见字符的ascii码之内

1 2	s.add(x < 127) s.add(x >= 32)

在约束条件时最好使用下标索引，用列表来管理（可以使输出是有序的）

1 2	s.add(s[18] * s[8] == 5) s.add(s[4] * s[11] == 0)

求解打印结果

answer=s.model() #求解
#print(answer)
result="".join([str(answer[i]) for i in s]) #连接
print(result)

z3.ArithRef

这个arithref，应该一开始使用z3的都会收到一个类型转换的报错。这是一个z3的特有变量类型，即使求解成功，也不能直接将这个类型的变量输出，在这里我们需要将变量进行类型转换才能成功的输出我们想要的数据。

m = s.model()
# 输出为int类型
a_int = m[a].as_long()
# 输出为fraction类型
d_float = m[d].as_fraction()

fraction类型的数据可以直接转换成float类型：

1 2	float(d_float) Out[31]: 3.0

一般来说不会整那些精度活，如果输出无理数那也没法转化成chr类型了，如果有那种报错在题里一般都是自己写错了，检查一下思路和数据。

例题

贴个normal8上去捏

from z3 import*
key = [0x00000008, 0x00000001, 0x00000007, 0x00000001, 0x00000001, 0x00000000, 0x00000004, 0x00000008, 0x00000001, 0x00000002, 0x00000003, 0x00000009, 0x00000003, 0x00000008, 0x00000006, 0x00000006, 0x00000004, 0x00000008, 0x00000003, 0x00000005, 0x00000007, 0x00000008, 0x00000008, 0x00000007, 0x00000000, 0x00000009, 0x00000000, 0x00000002, 0x00000003, 0x00000004, 0x00000002, 0x00000003, 0x00000002, 0x00000005, 0x00000004, 0x00000000, 0x00000000, 0x00000000, 0x00000000, 0x00000000]
str1 = [0x0000007A, 0x000000CF, 0x0000008C, 0x00000095, 0x0000008E, 0x000000A8, 0x0000005F, 0x000000C9, 0x0000007A, 0x00000091, 0x00000088, 0x000000A7, 0x00000070, 0x000000C0, 0x0000007F, 0x00000089, 0x00000086, 0x00000093, 0x0000005F, 0x000000CF, 0x0000006E, 0x00000086, 0x00000085, 0x000000AD, 0x00000088, 0x000000D4, 0x000000A0, 0x000000A2, 0x00000098, 0x000000B3, 0x00000079, 0x000000C1, 0x0000007E, 0x0000007E, 0x00000077, 0x00000093, 0x00000000, 0x00000000, 0x00000000, 0x00000000]
str2 = [0x00000010, 0x00000008, 0x00000008, 0x0000000E, 0x00000006, 0x0000000B, 0x00000005, 0x00000017, 0x00000005, 0x0000000A, 0x0000000C, 0x00000017, 0x0000000E, 0x00000017, 0x00000013, 0x00000007, 0x00000008, 0x0000000A, 0x00000004, 0x0000000D, 0x00000016, 0x00000011, 0x0000000B, 0x00000016, 0x00000006, 0x0000000E, 0x00000002, 0x0000000B, 0x00000012, 0x00000009, 0x00000005, 0x00000008, 0x00000008, 0x0000000A, 0x00000010, 0x0000000D]

s = Solver()

flag = [BitVec('%d' % i, 8) for i in range(36)]
flag1 = [0]*36
flag2 = [0]*36
str_1 = [0]*36
str_2 = [0]*36

for i in range(36):
    s.add(flag[i] < 127)
    s.add(flag[i] > 32)

flag1 = [(i >> 4) for i in flag]
flag2 = [(i & 0xf) for i in flag]


for i in range(6):
    for j in range(6):
        for k in range(6):
            str_1[6 * i + j] += flag1[6 * i + k] * key[6 * k + j]

for i in range(6):
    for j in range(6):
        str_2[6 * i + j] += flag2[6 * i + j] + key[6 * i + j]

for i in range(36):
    s.add(str_1[i] == str1[i])
    s.add(str_2[i] == str2[i])

if s.check() == sat:
    y = s.model()
    flag_ =  [chr(y[flag[i]].as_long().real) for i in range(36)]
    print(''.join(flag_))
else:
    print("Error!")

END

希望下次能自己写个出数据且不报错的z3（双手合十