首页
社区
课程
招聘
[原创]Z3求解约束器及例题
发表于: 2021-4-8 17:00 9897

[原创]Z3求解约束器及例题

2021-4-8 17:00
9897

在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        #若有解则得出解,注意这里的解是等式

[培训]内核驱动高级班,冲击BAT一流互联网大厂工作,每周日13:00-18:00直播授课

最后于 2021-4-22 17:37 被kanxue编辑 ,原因:
上传的附件:
收藏
免费 6
支持
分享
最新回复 (4)
雪    币: 38
能力值: ( LV1,RANK:0 )
在线值:
发帖
回帖
粉丝
2
tql!
2021-4-8 17:45
1
雪    币: 3668
活跃值: (9335)
能力值: ( LV9,RANK:319 )
在线值:
发帖
回帖
粉丝
3
互相进步,sr谦虚了
2021-4-8 19:04
1
雪    币: 529
活跃值: (1005)
能力值: ( LV2,RANK:10 )
在线值:
发帖
回帖
粉丝
4
直接复制粘贴别人的请注明出处。。一搜就有,不要当缝合怪
2021-4-9 11:49
1
雪    币: 3668
活跃值: (9335)
能力值: ( LV9,RANK:319 )
在线值:
发帖
回帖
粉丝
5

这是我自己的笔记哦,的确是综合了网上的一些文章,但是来源都比较零散,自己系统整理了一下,然后写了一道自己使用Z3解题的CTF题目,请问有什么问题吗。能找到和我这篇一样的文章说明你是看见我以前的csdn了。感谢提醒,以后如发文章时,会注意整理资料来源出处的,感谢提醒。

最后于 2021-4-9 13:37 被SYJ-Re编辑 ,原因:
2021-4-9 13:19
2
游客
登录 | 注册 方可回帖
返回
//