Z3在逆向中运用

发表于：2020-09-17 14:08 作者： Skye 阅读数（2005人）

文章共计7370个词

预计阅读10分钟

来和我一起阅读吧

≈≈≈≈≈≈≈≈≈≈≈≈≈≈≈

介绍

Z3 在工业应用中实际上常见于软件验证、程序分析等。然而由于功能实在强大，也被用于很多其他领域。CTF 领域来说，能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。此外，著名的二进制分析框架 angr 也内置了一个修改版的 Z3。

官方使用文档：https://rise4fun.com/z3/tutorialcontent/guide

z3py 功能手册：https://z3prover.github.io/api/html/namespacez3py.html

z3py 使用文档：https://ericpony.github.io/z3py-tutorial/guide-examples.htm

z3 所使用的语法标准：http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

安装

这里安装的是 python 库版本，编译好的二进制版本在 Github 下载。https://github.com/Z3Prover/z3/releases

简单使用

from z3 import *

x = Int('x')#设置整型变量x

y = Int('y')#设置整型变量y

solve(x > 2, y < 10, x + 2*y == 7)#写入方程

# [y = 0, x = 7]

进阶使用

设置变量

批量设置变量见补充

Int - 整数型

# 声明单个变量

x = Int('x')

# 声明多个变量

y,z = Ints('y z')

| 运算需要初始化为Int变量

Real - 实数型

# 声明单个变量

x = Real('x')

# 声明多个变量

y,z = Reals('y z')

BitVec - 向量（位运算）

# 声明单个 16 位的变量

x = BitVec('x',16)

# 声明多个 16 位的变量

y,z = BitVecs('y z',16)

只有 BitVec 变量可以进行异或

solver.add(BitVec('x',8)^BitVec('y',8)==5)

BitVec 变量值之间可进行>或<或=或>=或<=的比较

BitVec('a',8)>=BitVec('b',8)

BitVec('a',8)<=BitVec('b',8)

BitVec('a',8)<=9

BitVec('a',8)==9

BitVecVal 值之间不能进行>或<比较,只能转换成 python 认识的类型才可以比较

if BitVecVal(98,8)>BitVecVal(97,8)#错误，不是python类型

if BitVecVal(98,8)==98:

if BitVecVal(98,8).as_long()>97

if BitVecVal(98,8).as_long()>BitVecVal(97,8).as_long()

变量设置的类型可能会影响到最后求解的结果。可以先 check 一下看看有没有解，然后再判断是否需要切换变量的类型。

Solver 对象

实际做题时，约束条件肯定不会想上面例子这么少，所以需要实例化一个 Solver() 对象，方便我们添加更多的约束条件。

创建约束求解器：solver = Solver()

添加约束条件

一行一个约束条件，这里的约束条件就是方程等式：

solver.add(x**2+y**2==74)

solver.add(x**5-y==z)

# [y = -7, x = 5, z = 3132]

z3 中不允许列表与列表之间添加==约束条件：

判断是否有解

if solver.check() == sat:

print("solver")

else:

print("no solver")

求解并输出

ans = solver.model()

print(ans)

补充

限制结果为可见字符

通常如果是做题的话，解密出来很可能是 flag ，也就是 ascii 码，所以为了进一步约束范围可以给每一个变量都加上额外的一条约束，约束其结果只能在可见 ascii 码范围以内：

solver.add(x < 127)

solver.add(x >= 32)

快速添加变量

添加 50 个 Int 变量 s ：

s=[Int('s%d' % i) for i in range(50)]

添加 50 个 Real 变量 s ：

s=[Real('s%d' % i) for i in range(50)]

添加 50 个 16 位 BitVec 变量 s ：

s=[BitVec ('s%d' % i,16) for i in range(50)]

在约束条件中用下标索引使用：

solver.add(s[18] * s[8] == 5)

solver.add(s[4] * s[11] == 0)

将结果按顺序打印出来：

这是使用列表管理变量的好处，如果不使用列表 print(answer) 输出的结果是无序的。

answer=solver.model()

#print(answer)

result="".join([str(answer[each]) for each in s])

print(result)

练习例题

2020 羊城杯 login

题目前面还有一步逆向 pyinstaller 打包的 exe 文件，这里不赘述直接给出源码：

import sys

input1 = input('input something:')

if len(input1) != 14:

print('Wrong length!')

sys.exit()

code = []

for i in range(13):

code.append(ord(input1[i]) ^ ord(input1[i + 1]))

code.append(ord(input1[13]))

a1 = code[2]

a2 = code[1]

a3 = code[0]

a4 = code[3]

a5 = code[4]

a6 = code[5]

a7 = code[6]

a8 = code[7]

a9 = code[9]

a10 = code[8]

a11 = code[10]

a12 = code[11]

a13 = code[12]

a14 = code[13]

if ((((a1 * 88 + a2 * 67 + a3 * 65 - a4 * 5) + a5 * 43 + a6 * 89 + a7 * 25 + a8 * 13 - a9 * 36) + a10 * 15 + a11 * 11 + a12 * 47 - a13 * 60) + a14 * 29 == 22748) & ((((a1 * 89 + a2 * 7 + a3 * 12 - a4 * 25) + a5 * 41 + a6 * 23 + a7 * 20 - a8 * 66) + a9 * 31 + a10 * 8 + a11 * 2 - a12 * 41 - a13 * 39) + a14 * 17 == 7258) & ((((a1 * 28 + a2 * 35 + a3 * 16 - a4 * 65) + a5 * 53 + a6 * 39 + a7 * 27 + a8 * 15 - a9 * 33) + a10 * 13 + a11 * 101 + a12 * 90 - a13 * 34) + a14 * 23 == 26190) & ((((a1 * 23 + a2 * 34 + a3 * 35 - a4 * 59) + a5 * 49 + a6 * 81 + a7 * 25 + (a8 << 7) - a9 * 32) + a10 * 75 + a11 * 81 + a12 * 47 - a13 * 60) + a14 * 29 == 37136) & (((a1 * 38 + a2 * 97 + a3 * 35 - a4 * 52) + a5 * 42 + a6 * 79 + a7 * 90 + a8 * 23 - a9 * 36) + a10 * 57 + a11 * 81 + a12 * 42 - a13 * 62 - a14 * 11 == 27915) & ((((a1 * 22 + a2 * 27 + a3 * 35 - a4 * 45) + a5 * 47 + a6 * 49 + a7 * 29 + a8 * 18 - a9 * 26) + a10 * 35 + a11 * 41 + a12 * 40 - a13 * 61) + a14 * 28 == 17298) & ((((a1 * 12 + a2 * 45 + a3 * 35 - a4 * 9 - a5 * 42) + a6 * 86 + a7 * 23 + a8 * 85 - a9 * 47) + a10 * 34 + a11 * 76 + a12 * 43 - a13 * 44) + a14 * 65 == 19875) & (((a1 * 79 + a2 * 62 + a3 * 35 - a4 * 85) + a5 * 33 + a6 * 79 + a7 * 86 + a8 * 14 - a9 * 30) + a10 * 25 + a11 * 11 + a12 * 57 - a13 * 50 - a14 * 9 == 22784) & ((((a1 * 8 + a2 * 6 + a3 * 64 - a4 * 85) + a5 * 73 + a6 * 29 + a7 * 2 + a8 * 23 - a9 * 36) + a10 * 5 + a11 * 2 + a12 * 47 - a13 * 64) + a14 * 27 == 9710) & (((((a1 * 67 - a2 * 68) + a3 * 68 - a4 * 51 - a5 * 43) + a6 * 81 + a7 * 22 - a8 * 12 - a9 * 38) + a10 * 75 + a11 * 41 + a12 * 27 - a13 * 52) + a14 * 31 == 13376) & ((((a1 * 85 + a2 * 63 + a3 * 5 - a4 * 51) + a5 * 44 + a6 * 36 + a7 * 28 + a8 * 15 - a9 * 6) + a10 * 45 + a11 * 31 + a12 * 7 - a13 * 67) + a14 * 78 == 24065) & ((((a1 * 47 + a2 * 64 + a3 * 66 - a4 * 5) + a5 * 43 + a6 * 112 + a7 * 25 + a8 * 13 - a9 * 35) + a10 * 95 + a11 * 21 + a12 * 43 - a13 * 61) + a14 * 20 == 27687) & (((a1 * 89 + a2 * 67 + a3 * 85 - a4 * 25) + a5 * 49 + a6 * 89 + a7 * 23 + a8 * 56 - a9 * 92) + a10 * 14 + a11 * 89 + a12 * 47 - a13 * 61 - a14 * 29 == 29250) & (((a1 * 95 + a2 * 34 + a3 * 62 - a4 * 9 - a5 * 43) + a6 * 83 + a7 * 25 + a8 * 12 - a9 * 36) + a10 * 16 + a11 * 51 + a12 * 47 - a13 * 60 - a14 * 24 == 15317):

print('flag is GWHT{md5(your_input)}')

print('Congratulations and have fun!')

else:

print('Sorry,plz try again...')

import sys

input1 = input('input something:')

if len(input1) != 14:

print('Wrong length!')

sys.exit()

code = []

for i in range(13):

code.append(ord(input1[i]) ^ ord(input1[i + 1]))

code.append(ord(input1[13]))

a1 = code[2]

a2 = code[1]

a3 = code[0]

a4 = code[3]

a5 = code[4]

a6 = code[5]

a7 = code[6]

a8 = code[7]

a9 = code[9]

a10 = code[8]

a11 = code[10]

a12 = code[11]

a13 = code[12]

a14 = code[13]

print('flag is GWHT{md5(your_input)}')

print('Congratulations and have fun!')

else:

print('Sorry,plz try again...')

分析之后确定需要先求解出 a1~a14 的值，然后再经过一次异或获得 flag 。

这里我们手动添加多个变量，因为源码中的方式形式为 ax 。如果我们用列表管理变量，方程需要手动修改，消耗更多时间得不偿失。z3 脚本：

这里我们需要将有移位运算的那一条方程注释掉，因为 Int 没有这种运算方法。然后我们知道 a1~a14 是两两整数异或而来，所以加上约束大于等于 0 ，否则由于缺少一条方程解出来的值含有负数。

如果不想注释那条方程，完全使用全部方程，那么就将变量定义为：BitVec('an', 16) ，那么就能够使用移位运算。

然后就是还原异或加密：

a1 = 119

a2 = 24

a3 = 10

a4 = 7

a5 = 104

a6 = 43

a7 = 28

a8 = 91

a9 = 52

a10 = 108

a11 = 88

a12 = 74

a13 = 88#121

a14 = 33

code = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13]

code[0] = a3

code[1] = a2

code[2] = a1

code[3] = a4

code[4] = a5

code[5] = a6

code[6] = a7

code[7] = a8

code[9] = a9

code[8] = a10

code[10] = a11

code[11] = a12

code[12] = a13

code[13] = a14

flag = []

flag.append(chr(code[13]))

for i in list(range(13))[::-1]:

code[i] = (code[i] ^ code[i + 1])

for i in code:

print(chr(i),end='')

#flag:U_G07_th3_k3y!

2020 CISCN z3

用 IDA 分析题目得知，程序将输入值经过运算后与 Dst 的密文对比，也就是知道解，求出未知数。

Dst 定义是 int 型（8 字节），将密文提取出来：

de = [0x4F17,0x9CF6,0x8DDB,0x8EA6,0x6929,0x9911,0x40A2,0x2F3E,0x62B6,0x4B82,0x486C,0x4002,0x52D7,0x2DEF,0x28DC,0x640D,0x528F,0x613B,0x4781,0x6B17,0x3237,0x2A93,0x615F,0x50BE,0x598E,0x4656,0x5B31,0x313A,0x3010,0x67FE,0x4D5F,0x58DB,0x3799,0x60A0,0x2750,0x3759,0x8953,0x7122,0x81F9,0x5524,0x8971,0x3A1D]

这里还是用手动申请变量，因为避免修改方程表达式。这道例题可以用 Int 也可以用 BitVec ，这里就用 BitVec

from z3 import *

v46=BitVec('v46',8)

v47=BitVec('v47',8)

v48=BitVec('v48',8)

v49=BitVec('v49',8)

v50=BitVec('v50',8)

v51=BitVec('v51',8)

v52=BitVec('v52',8)

v53=BitVec('v53',8)

v54=BitVec('v54',8)

v55=BitVec('v55',8)

v56=BitVec('v56',8)

v57=BitVec('v57',8)

v58=BitVec('v58',8)

v59=BitVec('v59',8)

v60=BitVec('v60',8)

v61=BitVec('v61',8)

v62=BitVec('v62',8)

v63=BitVec('v63',8)

v64=BitVec('v64',8)

v65=BitVec('v65',8)

v66=BitVec('v66',8)

v67=BitVec('v67',8)

v68=BitVec('v68',8)

v69=BitVec('v69',8)

v70=BitVec('v70',8)

v71=BitVec('v71',8)

v72=BitVec('v72',8)

v73=BitVec('v73',8)

v74=BitVec('v74',8)

v75=BitVec('v75',8)

v76=BitVec('v76',8)

v77=BitVec('v77',8)

v78=BitVec('v78',8)

v79=BitVec('v79',8)

v80=BitVec('v80',8)

v81=BitVec('v81',8)

v82=BitVec('v82',8)

v83=BitVec('v83',8)

v84=BitVec('v84',8)

v85=BitVec('v85',8)

v86=BitVec('v86',8)

v87=BitVec('v87',8)

v4=de[0]

v5=de[1]

v6=de[2]

v7=de[3]

v8=de[4]

v9=de[5]

v10=de[6]

v11=de[7]

v12=de[8]

v13=de[9]

v14=de[10]

v15=de[11]

v16=de[12]

v17=de[13]

v18=de[14]

v19=de[15]

v20=de[16]

v21=de[17]

v22=de[18]

v23=de[19]

v24=de[20]

v25=de[21]

v26=de[22]

v27=de[23]

v28=de[24]

v29=de[25]

v30=de[26]

v31=de[27]

v32=de[28]

v33=de[29]

v34=de[30]

v35=de[31]

v36=de[32]

v37=de[33]

v38=de[34]

v39=de[35]

v40=de[36]

v41=de[37]

v42=de[38]

v43=de[39]

v44=de[40]

v45=de[41]

s=Solver()

s.add(v4 == 34 * v49 + 12 * v46 + 53 * v47 + 6 * v48 + 58 * v50 + 36 * v51 + v52)

s.add(v5 == 27 * v50 + 73 * v49 + 12 * v48 + 83 * v46 + 85 * v47 + 96 * v51 + 52 * v52)

s.add(v6 == 24 * v48 + 78 * v46 + 53 * v47 + 36 * v49 + 86 * v50 + 25 * v51 + 46 * v52)

s.add(v7 == 78 * v47 + 39 * v46 + 52 * v48 + 9 * v49 + 62 * v50 + 37 * v51 + 84 * v52)

s.add(v8 == 48 * v50 + 14 * v48 + 23 * v46 + 6 * v47 + 74 * v49 + 12 * v51 + 83 * v52)

s.add(v9 == 15 * v51 + 48 * v50 + 92 * v48 + 85 * v47 + 27 * v46 + 42 * v49 + 72 * v52)

s.add(v10 == 26 * v51 + 67 * v49 + 6 * v47 + 4 * v46 + 3 * v48 + 68 * v52)

s.add(v11 == 34 * v56 + 12 * v53 + 53 * v54 + 6 * v55 + 58 * v57 + 36 * v58 + v59)

s.add(v12 == 27 * v57 + 73 * v56 + 12 * v55 + 83 * v53 + 85 * v54 + 96 * v58 + 52 * v59)

s.add(v13 == 24 * v55 + 78 * v53 + 53 * v54 + 36 * v56 + 86 * v57 + 25 * v58 + 46 * v59)

s.add(v14 == 78 * v54 + 39 * v53 + 52 * v55 + 9 * v56 + 62 * v57 + 37 * v58 + 84 * v59)

s.add(v15 == 48 * v57 + 14 * v55 + 23 * v53 + 6 * v54 + 74 * v56 + 12 * v58 + 83 * v59)

s.add(v16 == 15 * v58 + 48 * v57 + 92 * v55 + 85 * v54 + 27 * v53 + 42 * v56 + 72 * v59)

s.add(v17 == 26 * v58 + 67 * v56 + 6 * v54 + 4 * v53 + 3 * v55 + 68 * v59)

s.add(v18 == 34 * v63 + 12 * v60 + 53 * v61 + 6 * v62 + 58 * v64 + 36 * v65 + v66)

s.add(v19 == 27 * v64 + 73 * v63 + 12 * v62 + 83 * v60 + 85 * v61 + 96 * v65 + 52 * v66)

s.add(v20 == 24 * v62 + 78 * v60 + 53 * v61 + 36 * v63 + 86 * v64 + 25 * v65 + 46 * v66)

s.add(v21 == 78 * v61 + 39 * v60 + 52 * v62 + 9 * v63 + 62 * v64 + 37 * v65 + 84 * v66)

s.add(v22 == 48 * v64 + 14 * v62 + 23 * v60 + 6 * v61 + 74 * v63 + 12 * v65 + 83 * v66)

s.add(v23 == 15 * v65 + 48 * v64 + 92 * v62 + 85 * v61 + 27 * v60 + 42 * v63 + 72 * v66)

s.add(v24 == 26 * v65 + 67 * v63 + 6 * v61 + 4 * v60 + 3 * v62 + 68 * v66)

s.add(v25 == 34 * v70 + 12 * v67 + 53 * v68 + 6 * v69 + 58 * v71 + 36 * v72 + v73)

s.add(v26 == 27 * v71 + 73 * v70 + 12 * v69 + 83 * v67 + 85 * v68 + 96 * v72 + 52 * v73)

s.add(v27 == 24 * v69 + 78 * v67 + 53 * v68 + 36 * v70 + 86 * v71 + 25 * v72 + 46 * v73)

s.add(v28 == 78 * v68 + 39 * v67 + 52 * v69 + 9 * v70 + 62 * v71 + 37 * v72 + 84 * v73)

s.add(v29 == 48 * v71 + 14 * v69 + 23 * v67 + 6 * v68 + 74 * v70 + 12 * v72 + 83 * v73)

s.add(v30 == 15 * v72 + 48 * v71 + 92 * v69 + 85 * v68 + 27 * v67 + 42 * v70 + 72 * v73)

s.add(v31 == 26 * v72 + 67 * v70 + 6 * v68 + 4 * v67 + 3 * v69 + 68 * v73)

s.add(v32 == 34 * v77 + 12 * v74 + 53 * v75 + 6 * v76 + 58 * v78 + 36 * v79 + v80)

s.add(v33 == 27 * v78 + 73 * v77 + 12 * v76 + 83 * v74 + 85 * v75 + 96 * v79 + 52 * v80)

s.add(v34 == 24 * v76 + 78 * v74 + 53 * v75 + 36 * v77 + 86 * v78 + 25 * v79 + 46 * v80)

s.add(v35 == 78 * v75 + 39 * v74 + 52 * v76 + 9 * v77 + 62 * v78 + 37 * v79 + 84 * v80)

s.add(v36 == 48 * v78 + 14 * v76 + 23 * v74 + 6 * v75 + 74 * v77 + 12 * v79 + 83 * v80)

s.add(v37 == 15 * v79 + 48 * v78 + 92 * v76 + 85 * v75 + 27 * v74 + 42 * v77 + 72 * v80)

s.add(v38 == 26 * v79 + 67 * v77 + 6 * v75 + 4 * v74 + 3 * v76 + 68 * v80)

s.add(v39 == 34 * v84 + 12 * v81 + 53 * v82 + 6 * v83 + 58 * v85 + 36 * v86 + v87)

s.add(v40 == 27 * v85 + 73 * v84 + 12 * v83 + 83 * v81 + 85 * v82 + 96 * v86 + 52 * v87)

s.add(v41 == 24 * v83 + 78 * v81 + 53 * v82 + 36 * v84 + 86 * v85 + 25 * v86 + 46 * v87)

s.add(v42 == 78 * v82 + 39 * v81 + 52 * v83 + 9 * v84 + 62 * v85 + 37 * v86 + 84 * v87)

s.add(v43 == 48 * v85 + 14 * v83 + 23 * v81 + 6 * v82 + 74 * v84 + 12 * v86 + 83 * v87)

s.add(v44 == 15 * v86 + 48 * v85 + 92 * v83 + 85 * v82 + 27 * v81 + 42 * v84 + 72 * v87)

s.add(v45 == 26 * v86 + 67 * v84 + 6 * v82 + 4 * v81 + 3 * v83 + 68 * v87)

print(s.check())

flag=""

if s.check() == sat:

m = s.model()

print(m)

else:

print("no answer")

flag = ""

for d in m.decls():

print("%s = %s" % (d.name(), m[d]))

极客大挑战 REConvolution

这条题目演示用批量申请堆方法

题目关键函数：

加密过程并不是前两题的方程了，而是循环异或，没有修改方程变量名的问题，所以我们可以用 for 循环申请变量。

数独

z3 还能处理数独问题，下面是官方 demo ：

#!/usr/bin/env python

# -*- coding: utf-8 -*-

# @Author : MrSkYe

# @Email : skye231@foxmail.com

from z3 import *

# 9x9整数变量矩阵

X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]

for i in range(9) ]

# 每个单元格包含{1，…，9}中的值

cells_c = [ And(1 <= X[i][j], X[i][j] <= 9)

for i in range(9) for j in range(9) ]

# 每行最多包含一个数字一次

rows_c = [ Distinct(X[i]) for i in range(9) ]

# 每列最多包含一个数字

cols_c = [ Distinct([ X[i][j] for i in range(9) ])

for j in range(9) ]

# 每个3x3正方形最多包含一个数字

sq_c = [ Distinct([ X[3*i0 + i][3*j0 + j]

for i in range(3) for j in range(3) ])

for i0 in range(3) for j0 in range(3) ]

sudoku_c = cells_c + rows_c + cols_c + sq_c

# 数独实例，我们用'0'表示空单元格

instance = ((0,0,0,0,9,4,0,3,0),

(0,0,0,5,1,0,0,0,7),

(0,8,9,0,0,0,0,4,0),

(0,0,0,0,0,0,2,0,8),

(0,6,0,2,0,1,0,5,0),

(1,0,2,0,0,0,0,0,0),

(0,7,0,0,0,0,5,2,0),

(9,0,0,0,6,5,0,0,0),

(0,4,0,9,7,0,0,0,0))

instance_c = [ If(instance[i][j] == 0,

True,

X[i][j] == instance[i][j])

for i in range(9) for j in range(9) ]

s = Solver()

s.add(sudoku_c + instance_c)

if s.check() == sat:

m = s.model()

r = [ [ m.evaluate(X[i][j]) for j in range(9) ]

for i in range(9) ]

print_matrix(r)

else:

print("failed to solve")

参考文章

Z3 学习笔记 https://blog.csdn.net/qq_33438733/article/details/82011892)

z3 solver学习 http://3xp10it.cc/auxilary/2017/11/14/z3-solver%E5%AD%A6%E4%B9%A0/)

实验推荐--CTF-REVERSE练习之逆向初探 （本实验将通过具体的实例介绍Ollydbg/IDA Pro/PEiD等工具在逆向分析中的基本使用方法，并通过动态调试和静态分析两种方法来找到程序密码。）