首页
论坛
课程
招聘
[Reverse] [原创]Z3求解约束器及例题
2021-4-8 17:00 898

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

2021-4-8 17:00
898

Z3求解约束器

一:基本数据类型:

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

1
2
3
4
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
5
6
7
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
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
olver.add()

判断解是否存在

1
if solver.check()==sat:

求解

1
print solver.model()

三:z3的简单使用及ctf实例

例一

 

假设有方程组:

1
2
30x+15y=675
12x+5y=265

完整代码:

1
2
3
4
5
6
7
8
9
10
11
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

例二

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
>>> from z3 import *
>>> x = Int('x')
>>> y = Int('y')
>>> a = Real('a')
>>> b = Real('b')
>>> c = Real('c')
>>> d = Real('d')       #设未知数
>>> s = Solver()        #创建约束求解器
>>> s.add(a + b == 12#在约束求解器下添加约束条件
>>> s.add(c - d == 9)    
>>> s.add(a + c == 22)
>>> s.add(b + d == 12)
>>>
>>> print(s.check())   #检测是否有解
sat
>>> print(s.model())   #打印出求解的结果
[b = 11/2, a = 13/2, d = 13/2, c = 31/2]
>>> p = Solver()
>>> p.add(x + y == 1567856551)
>>> p.add(x - y == 6535435)
>>> p.check()
sat
>>> p.model()
[x = 787195993, y = 780660558]

例三:

 

这里放一道使用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版本

  1. 写出脚本
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
44
45
46
from z3 import *       #若导入了模块但没有使用则是这种灰色
arr1 = [0X7A,0XCF,0X8C,0X95,0X8E,0XA8,0X5F,0XC9,0X7A,0X91,0X88,0XA7,0X70,0XC0,0X7F,0X89,0X86,0X93,0X5F,0XCF,0X6E,0X86,
        0X85,0XAD,0X88,0XD4,0XA0,0XA2,0X98,0XB3,0X79,0XC1,0X7E,0X7E,0X77,0X93]
arr2 = [0x10,0x08,0X08,0x0E,0X06,0X0B,0X5,0X17,0X05,0X0A,0X0C,0X17,0X0E,0X17,0X13,0X07,0X08,0X0A,0X04,0X0D,0X16,0X11,0X0B,
        0X16,0X06,0X0E,0X02,0X0B,0X12,0X09,0X05,0X08,0X08,0X0A,0X10,0X0D]
arr3 = [8,1,7,1,1,0,4,8,1,2,3,9,3,8,6,6,4,8,3,5,7,8,8,7,0,9,0,2,3,4,2,3,2,5,4,0]
#学会了idapython将其提取出来,arr1对应v8,arr2对应v9,arr3对应unk_602080
temp = [BitVec('%d' % i, 8) for i in range(36)]  #初始化序列
s = Solver()     #创建约束求解器
for i in range(36):
    s.add(temp[i] <127)   #添加约束条件①
    s.add(temp[i] >=32)
#接下来还原代码
ptr = [0]*36
v7 = [0]*36   #最开始的两个变换之后的数组
one = [0]*36
two = [0]*36    #这两个用来存放对应的两个函数的结果
for i in range(36):
    ptr[i] = temp[i] >> 4
    v7[i] = temp[i] & 15
for i in range(6):
    for j in range(6):
        for k in range(6):
            one[6*i+j] += ptr[6*i + k] * arr3[6*k+j]
 
for i in range(6):
    for j in range(6):
        two[6*i+j] = v7[6*i+j] + arr3[6*i+j]
#代码还原结束
for i in range(36):          #添加约束条件②
    s.add(one[i] == arr1[i])
    s.add(two[i] == arr2[i])
flag = []
strflag = ''
if s.check() == sat:     #检测是否有解
    result = s.model()
    for i in temp:       #因为最后得出的是等式,先遍历temp,把temp的每个依次赋给i
        flag.append(result[i])    #然后找到每个temp对应的解,附加到空列表的后面
    print(flag)          #这里先打印出来,然后后面重新赋一个序列
else:
    print('无解')
 
result = [104, 103, 97, 109, 101, 123, 49, 95, 116, 104, 105, 110, 107, 95, 77, 97, 116, 114, 49, 120, 95, 105, 115, 95, 118, 101, 114, 121, 95, 117, 115, 101, 102, 53, 108, 125]
for i in range(36):
    strflag += chr(result[i])
print(strflag)

运行结果:

 

图片描述

 

得到flag为:

 

hgame{1_think_Matr1x_is_very_usef5l}


[公告]春风十里不如你,看雪团队诚邀你的加入!

最后于 2021-4-8 17:05 被SYJ-Re编辑 ,原因:
收藏
点赞1
打赏
分享
最新回复 (4)
雪    币: 43
能力值: ( LV1,RANK:0 )
在线值:
发帖
回帖
粉丝
郁雨 活跃值 2021-4-8 17:45
2
1
tql!
雪    币: 811
活跃值: 活跃值 (820)
能力值: ( LV4,RANK:40 )
在线值:
发帖
回帖
粉丝
SYJ-Re 活跃值 2021-4-8 19:04
3
1
互相进步,sr谦虚了
雪    币: 460
活跃值: 活跃值 (699)
能力值: ( LV2,RANK:10 )
在线值:
发帖
回帖
粉丝
_air 活跃值 2021-4-9 11:49
4
1
直接复制粘贴别人的请注明出处。。一搜就有,不要当缝合怪
雪    币: 811
活跃值: 活跃值 (820)
能力值: ( LV4,RANK:40 )
在线值:
发帖
回帖
粉丝
SYJ-Re 活跃值 2021-4-9 13:19
5
2

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

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