-
-
[原创]Z3求解约束器及例题
-
发表于: 2021-4-8 17:00
-
在Python中使用Z3模块，我们的所求结果一般有以下几种数据类型:
其中BitVec可以是特定大小的数据类型，不一定是8，例如C语言中的int型可以用BitVec('a',32)表示
设未知数的方法：
可以使用'Int','Real','BitVec'等声明一个整数或实数变量，也可以申明一个变量数组
例如：x = Int('x') #这个int不是c/c++中的那个，而仅仅只代表整数
初始化序列：
Solver()
Solver()命令会创建一个通用求解器，创建后我们可以添加我们的约束条件，进行下一步的求解
add()
add()命令用来添加约束条件，通常在solver()命令之后，添加的约束条件通常是一个逻辑等式
check()
该函数通常用来判断在添加完约束条件后，来检测解的情况，有解的时候会回显sat，无解的时候会回显unsat
model()
在存在解的时候，该函数会将每个限制条件所对应的解集的交集，进而得出正解。
常用求解四步骤：
创建约束求解器
添加约束条件（这一步是z3求解的关键）
判断解是否存在
求解
例一：
假设有方程组：
完整代码：
例二：
例三：
这里放一道使用Z3解的CTF题目：
链接：https://pan.baidu.com/s/1aUwsbaS3d1ducOjKVVc0VA
提取码：0syj
Write Up By SYJ
拖入IDA进行分析
找到关键代码:
就是这几个关键部分，还是可以很清楚的把它分析出来
首先for循环对输入的字符进行处理，然后得到ptr数组和v7数组，长度都为36
分析sub_40078E函数：
可以发现有三个for循环，是对传进的两个数组进行了相乘的运算。
分析sub_400892函数：
可以发现是数组进行了相加的运算
最后就是将两个函数得到的数组中的值与程序中数据的值进行对比。
思路：本来想直接用for i in range(32,127):但是这个只能一个一个的爆破，但是很明显他是直接取的未知数的数组，这个就不可行了
得用z3求解约束器(使用pip安装：pip install z3-solver)
1.
先用idapython将对应地址的数据进行导出：
图中的ida是基于7.5版本
运行结果:
得到flag为：
hgame{1_think_Matr1x_is_very_usef5l}
Int #整型
Bool #布尔型
Array #数组
BitVec('a',8) #char型
Int #整型
Bool #布尔型
Array #数组
BitVec('a',8) #char型
y = Real('y') #**实数**变量(**数学中的**那个实数)
z = BitVec('z',8) #char型
w = BitVec('w',32) #int型
p = Bool('p') #定义布尔型
y = Real('y') #**实数**变量(**数学中的**那个实数)
z = BitVec('z',8) #char型
w = BitVec('w',32) #int型
p = Bool('p') #定义布尔型
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]
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()
solver = Solver()
olver.add()olver.add()if solver.check()==sat:
if solver.check()==sat:
print solver.model()
print solver.model()
30x+15y=675
12x+5y=265
30x+15y=675
12x+5y=265
from z3 import *
x = Real('x')
y = Real('y') #设未知数
s = Solver() #创建约束求解器
s.add(30*x+15*y==675)
s.add(12*x+5*y==265) #添加约束条件
if s.check() == sat: #检测是否有解
result = s.model()
print result #若有解则得出解，注意这里的解是等式
else:
print 'no result' #无解则打印no result
from z3 import *
x = Real('x')
y = Real('y') #设未知数
s = Solver() #创建约束求解器
s.add(30*x+15*y==675)
s.add(12*x+5*y==265) #添加约束条件
if s.check() == sat: #检测是否有解
result = s.model()
print result #若有解则得出解，注意这里的解是等式
[注意]传递专业知识、拓宽行业人脉——看雪讲师团队等你加入！
|
|
|---|---|
|
|
|
|
|
|
|
|
|
|
|
|
