-
-
[原创]Z3求解约束器及例题
-
2021-4-8 17:00
-
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=67512x+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 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_602080temp = [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]*36v7 = [0]*36 #最开始的两个变换之后的数组one = [0]*36two = [0]*36 #这两个用来存放对应的两个函数的结果for i in range(36): ptr[i] = temp[i] >> 4 v7[i] = temp[i] & 15for 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}
|
|
|---|---|
|
|
|
|
|
|
|
|
|
|
|
|
