• 新闻动态
  • 行业动态
  • 公司新闻
  • 关于我们
  • 公司简介
  • 经典活动
  • 经验总结
    Z3在逆向中运用
    2020-09-17 13:35

    文章共计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

    1.png

    简单使用

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

    2.png

    判断是否有解

    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]

    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 脚本:

    3.png

    4.png

    5.png

    这里我们需要将有移位运算的那一条方程注释掉,因为 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 *


    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

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

    题目关键函数:

    6.png

    7.png

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


    8.png

    数独

    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等工具在逆向分析中的基本使用方法,并通过动态调试和静态分析两种方法来找到程序密码。)

    9.png

    上一篇:逆向入门分析实战(四)
    下一篇:Java-Web之s2-001与CommonsCollections
    版权所有 合天智汇信息技术有限公司 2013-2020 湘ICP备14001562号-6
    Copyright © 2013-2020 Heetian Corporation, All rights reserved
    4006-123-731