Z3求解约束器

基本数据类型 :

在Python中使用Z3模块，我们的所求结果一般有以下几种数据类型:

Int #整型
Bool #布尔型
Array #数组
BitVec ( ‘a’，8 ) #char型

其中BitVec可以是特定大小的数据类型，不一定是8，例如C语言中的int型可以用BitVec(‘a’,32)表示

设未知数的方法 ：

可以使用 ‘Int’ , ‘Real’ , ‘BitVec’ 等声明一个整数或实数变量，也可以申明一个变量数组

例如：x = Int(‘x’) #这个int不是c/c++中的那个，而仅仅只代表整数

1
2
3
4
y =Real('y')  				#实数变量(数学中的那个实数)
z =BitVec('z',8) 			#char型
w =BitVec('w',32) 			#int型
p =Bool('p')    			#定义布尔型

初始化序列：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

flag = []
for i in range(5):
    flag.append(BitVec('%d' % i, 8))    #char型
print(flag)
 
#结果为:[0, 1, 2, 3, 4]
 
flag= [Int('%d' % i) for i in range(32)]    #初始化为int型
 
flag = []
for i in range(5):
    flag.append(BitVec('%d' % i, 32))    #int型
print(flag)
 
#结果为:[0, 1, 2, 3, 4]

二：基本使用语法:

Solver()

Solver()命令会创建一个通用求解器，创建后我们可以添加我们的约束条件，进行下一步的求解

add()

add()命令用来添加约束条件，通常在solver()命令之后，添加的约束条件通常是一个逻辑等式

check()

该函数通常用来判断在添加完约束条件后，来检测解的情况，有解的时候会回显sat，无解的时候会回显unsat

model()

在存在解的时候，该函数会将每个限制条件所对应的解集的交集，进而得出正解。

常用求解步骤：

创建约束求解器

1
solver = Solver()

添加约束条件（这一步是z3求解的关键）

1
solver.add()

判断解是否存在

1
if solver.check() == sat:		# sat 表示有解 unsat 表示无解

求解

1
print ( solver.model() )		#一般是以 '约束求解器'.model() 得到结果，配合 print输出

题目示例

尝试求解 try 部分内容 ：

其中的 key_cmp 对应的分别为 S y c l o v e r

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43

from z3 import *



key1 = BitVec('key1',32)		#之前改了下面的数据不想改回去偷了个懒没写成数组
key2 = BitVec('key2',32)
key3 = BitVec('key3',32)
key4 = BitVec('key4',32)
key5 = BitVec('key5',32)
key6 = BitVec('key6',32)
key7 = BitVec('key7',32)
key8 = BitVec('key8',32)



key = Solver()					#创建约束求解器

key.add((key2 * key3 - key6 * 72 - key5 * 3 - key4 ^ key2 + (key4 << 2) + key3 * 6 - key8 & key7 - 1000) - 14==ord('S'))


key.add(((key6 * 7 + key4 * 3 + key3 + key7 - (key3 >> 2) - key2 ^ key1 + key8 + (key5 ^ key2) + (key5 | key8)) - 801)==ord('y'))

key.add(((key7 * 5 + key3 * 6 - key4 * 7 + key5 | key6 + key5 * 10 + key1 ^ key2 * 3 - key8 + key1 + key2) - 924)==ord('c'))

key.add((key2 * 3 + key6 * 9 + key1 + key3 * 2 + key4 * 5 - key5 * (key7 ^ key8) + 321 - 16)==ord('l'))

key.add(((key6 * 12 - key1 ^ key7 - key4 * 23 + key5 * 3 + key3 * 8 + key2 - key8 * 2 + key7 * 4 + 1324) + 1)==ord('o'))

key.add((key4 * 54 - key2 * 3 + key3 * 3 + key5 * 11 - key6 * 2 + key1 + key8 * 3 - key7 - 6298 + 40)==ord('v'))

key.add((key8 - key7 * key4 + key3 * key3 - key5 * 32 + key6 * (key1 >> 2) - key2 * key2 - 6689 + 41)==ord('e'))

key.add(((key6 - key4 * 41 + key7 * 41 + key6 ^ (key5 & key7 | key1) - (key8 * 24 | key3) + key2 - 589) - 36)==ord('r'))

#约束条件

if key.check()==sat:			#判断解的情况
    print(key.model())			#输出解
else:
    print("WA")


输出为 ：

Crypto
Z3求解约束器
https://equinox-shame.github.io/2022/03/14/Z3求解约束器/
作者
梓曰
发布于
2022年3月14日
许可协议