在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
)
Int
Bool
Array
BitVec(
'a'
,
8
)
y
=
Real(
'y'
)
z
=
BitVec(
'z'
,
8
)
w
=
BitVec(
'w'
,
32
)
p
=
Bool
(
'p'
)
y
=
Real(
'y'
)
z
=
BitVec(
'z'
,
8
)
w
=
BitVec(
'w'
,
32
)
p
=
Bool
(
'p'
)
flag
=
[]
for
i
in
range
(
5
):
flag.append(BitVec(
'%d'
%
i,
8
))
print
(flag)
结果为:[
0
,
1
,
2
,
3
,
4
]
flag
=
[
Int
(
'%d'
%
i)
for
i
in
range
(
32
)]
flag
=
[]
for
i
in
range
(
5
):
flag.append(BitVec(
'%d'
%
i,
32
))
print
(flag)
结果为:[
0
,
1
,
2
,
3
,
4
]
flag
=
[]
for
i
in
range
(
5
):
flag.append(BitVec(
'%d'
%
i,
8
))
print
(flag)
结果为:[
0
,
1
,
2
,
3
,
4
]
flag
=
[
Int
(
'%d'
%
i)
for
i
in
range
(
32
)]
flag
=
[]
for
i
in
range
(
5
):
flag.append(BitVec(
'%d'
%
i,
32
))
print
(flag)
结果为:[
0
,
1
,
2
,
3
,
4
]
solver
=
Solver()
olver.add()
if
solver.check()
=
=
sat:
print
solver.model()
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'
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
[培训]内核驱动高级班,冲击BAT一流互联网大厂工作,每周日13:00-18:00直播授课
最后于 2021-4-22 17:37
被kanxue编辑
,原因: