Z3在逆向中运用

  • A+
所属分类:逆向工程
Z3在逆向中运用
亲爱的,关注我吧
Z3在逆向中运用

9/17

文章共计7370个词

预计阅读10分钟

来和我一起阅读吧


介绍

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

官方使用文档:https://rise4fun.com/z3/tutorialcontent/guidez3py 功能手册:https://z3prover.github.io/api/html/namespacez3py.htmlz3py 使用文档:https://ericpony.github.io/z3py-tutorial/guide-examples.htmz3 所使用的语法标准:http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

安装

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

Z3在逆向中运用


简单使用

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 中不允许列表与列表之间添加==约束条件:

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 sysinput1 = 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 sysinput1 = 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...')


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

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

Z3在逆向中运用

Z3在逆向中运用

Z3在逆向中运用

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

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

然后就是还原异或加密:

a1 = 119a2 = 24a3 = 10a4 = 7a5 = 104a6 = 43a7 = 28a8 = 91a9 = 52a10 = 108a11 = 88a12 = 74a13 = 88#121a14 = 33
code = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13]
code[0] = a3code[1] = a2code[2] = a1code[3] = a4code[4] = a5code[5] = a6code[6] = a7code[7] = a8code[9] = a9code[8] = a10code[10] = a11code[11] = a12code[12] = a13code[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 *
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]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

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

题目关键函数:

Z3在逆向中运用

Z3在逆向中运用

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

Z3在逆向中运用


数独

z3 还能处理数独问题,下面是官方 demo :

#!/usr/bin/env python# -*- coding: utf-8 -*-# @Author  : MrSkYe# @Email   : [email protected]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练习之逆向初探 https://www.hetianlab.com/expc.do?ec=ECID172.19.104.182014111410002900001(本实验将通过具体的实例介绍Ollydbg/IDA Pro/PEiD等工具在逆向分析中的基本使用方法,并通过动态调试和静态分析两种方法来找到程序密码。)


Z3在逆向中运用



Z3在逆向中运用
“阅读原文”我们一起学习

发表评论

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: