z3在逆向中的应用

from z3 import *

# 下面是从ida提取出来的数据，每一行的“大数”是“=”左边，剩下的是“=”右边的未知数系数
# 共 42 行，42个未知数，可解，但我必不可能手算
pre = "234923  89 30 21 11 28 97 68 91 36 29 54 38 18 31 27 25 42 93 45 89 80 94 57 68 59 75 74 47 40 25 68 52 86 81 " \
      "38 23 90 80 54 66 80 36\x0A233479  65 11 81 65 58 53 86 44 62 39 64 41 93 67 34 30 25 45 76 17 91 47 57 82 26 " \
      "17 94 51 21 80 59 26 75 75 25 67 52 23 81 57 79 98\x0A231388  63 83 55 29 57 53 31 99 27 92 85 98 63 80 18 78 " \
      "79 28 96 16 95 27 25 71 40 89 79 81 13 85 41 44 50 55 11 32 76 65 20 37 58 27\x0A223405  39 69 44 25 49 15 16 " \
      "96 35 32 92 95 11 58 31 90 67 72 83 78 15 25 93 96 97 31 58 59 14 86 36 37 22 75 43 72 13 26 18 64 64 " \
      "83\x0A234762  94 82 88 51 31 71 44 74 26 46 95 66 54 75 19 72 93 16 85 54 46 87 15 46 74 27 26 48 83 13 38 94 " \
      "45 52 24 72 59 71 32 65 24 93\x0A242484  34 75 68 93 79 19 14 76 60 69 73 29 48 61 49 64 98 29 77 81 85 11 87 " \
      "11 72 63 87 40 47 48 87 54 88 27 26 67 93 50 79 42 12 32\x0A232356  76 61 21 72 11 93 13 63 15 13 73 49 48 76 " \
      "52 81 62 78 84 79 95 74 57 21 13 95 15 93 57 38 89 98 68 69 21 40 20 55 62 29 54 40\x0A239858  98 66 92 23 97 " \
      "55 72 69 81 41 38 21 56 95 86 39 78 53 65 37 80 56 38 60 94 72 20 43 50 28 81 63 12 60 32 12 22 86 65 32 76 " \
      "71\x0A218896  32 15 73 84 27 21 74 21 35 26 85 28 57 91 37 12 67 47 10 74 62 53 73 84 94 46 74 47 57 40 88 71 " \
      "13 32 81 95 57 28 13 94 45 34\x0A249026  50 47 34 57 12 34 76 54 79 18 44 73 50 92 51 72 39 91 26 74 97 42 86 " \
      "79 53 50 62 14 71 55 87 64 77 62 63 48 27 81 93 85 65 83\x0A222855  92 26 78 74 25 38 64 98 68 71 14 99 92 11 " \
      "31 29 20 52 17 10 21 37 99 52 66 32 57 58 25 25 93 54 96 70 18 66 84 27 44 28 52 83\x0A210754  53 39 23 68 62 " \
      "44 98 17 80 16 63 51 15 49 84 23 97 26 65 35 11 83 43 64 21 39 37 79 73 61 55 57 58 69 16 10 48 86 80 13 67 " \
      "32\x0A261049  12 69 82 77 95 22 21 85 79 58 48 83 47 77 64 80 56 35 78 67 46 93 51 75 69 62 44 11 46 98 37 93 " \
      "34 53 87 46 85 79 69 81 45 86\x0A254017  51 74 62 62 86 10 49 94 65 50 62 95 48 66 14 84 61 41 89 78 46 60 20 " \
      "97 32 65 61 78 57 16 64 97 81 81 76 61 27 46 99 64 35 99\x0A202040  15 47 16 70 28 32 65 82 53 32 29 25 69 96 " \
      "52 76 22 41 82 91 47 24 55 40 18 19 52 83 37 51 89 37 27 55 40 82 61 27 26 28 30 73\x0A213614  11 29 51 69 81 " \
      "96 58 97 36 81 18 62 73 32 72 11 49 61 69 67 54 30 10 70 42 27 19 11 97 83 27 40 63 12 41 21 84 74 22 19 65 " \
      "79\x0A246738  76 64 47 17 80 57 93 11 79 98 56 86 23 67 63 11 54 72 80 44 50 61 14 43 80 48 63 52 99 79 40 64 " \
      "49 55 52 78 48 60 44 32 85 98\x0A204859  77 34 26 66 87 76 58 39 81 60 83 23 16 62 33 36 85 40 64 78 22 11 81 " \
      "81 27 12 11 41 15 19 69 20 26 66 17 87 50 67 47 21 31 81\x0A248644  56 66 51 80 33 73 76 42 13 91 75 90 82 20 " \
      "15 99 33 18 22 28 39 17 74 54 78 47 61 68 73 95 60 52 84 11 78 67 82 79 31 94 78 74\x0A227559  24 15 63 20 81 " \
      "71 50 77 98 71 98 43 57 10 66 53 36 45 44 54 90 22 96 68 98 27 71 78 37 43 20 50 82 84 19 76 59 27 47 31 19 " \
      "31\x0A215120  45 66 23 77 41 65 99 35 67 29 63 77 55 36 27 63 43 70 55 11 28 17 77 90 28 57 62 98 84 96 36 43 " \
      "30 73 32 25 34 14 91 18 73 26\x0A218244  65 25 41 22 34 46 91 70 35 22 65 60 96 58 76 80 21 62 59 70 51 50 39 " \
      "14 31 39 79 49 45 82 74 35 56 24 93 47 32 41 14 15 71 51\x0A229321  45 99 29 14 89 72 48 43 92 10 94 13 33 94 " \
      "59 22 65 29 23 86 67 83 28 46 83 89 48 59 28 38 82 32 70 50 28 39 24 60 17 37 60 90\x0A233372  62 66 17 38 19 " \
      "83 12 98 61 57 63 67 69 10 24 75 60 87 76 37 91 35 20 30 24 77 29 27 40 36 98 82 20 67 45 96 99 80 17 55 74 " \
      "55\x0A251643  64 68 36 79 23 96 16 40 79 16 85 77 99 56 95 99 60 28 11 96 22 66 47 66 90 48 80 34 22 47 66 80 " \
      "37 43 75 84 23 21 39 85 64 95\x0A245051  14 55 61 90 62 91 24 31 40 34 88 59 65 26 16 28 36 33 81 91 99 57 69 " \
      "75 32 98 17 60 94 16 89 51 35 74 87 98 52 39 73 41 65 65\x0A228339  58 64 96 49 96 43 13 28 42 90 80 33 68 62 " \
      "42 78 75 56 20 66 45 63 10 72 41 63 28 42 60 26 76 20 98 19 51 68 80 12 48 68 80 15\x0A271672  93 74 76 39 79 " \
      "99 22 66 47 40 85 58 50 56 84 93 65 65 56 66 95 32 84 48 51 68 30 96 93 60 83 79 54 61 99 77 12 51 31 93 54 " \
      "12\x0A207826  30 29 52 29 91 81 31 28 75 84 10 40 14 34 26 70 94 74 27 38 55 13 21 55 79 94 45 41 39 62 56 25 " \
      "10 54 61 58 23 97 95 70 18 62\x0A208076  19 60 27 79 53 21 21 47 52 26 42 82 20 87 74 57 88 22 67 95 69 24 50 " \
      "14 31 26 38 40 31 46 17 67 85 54 33 46 43 72 84 94 67 29\x0A230168  37 52 47 30 99 11 20 20 41 72 46 78 97 93 " \
      "47 73 48 35 85 99 77 49 48 75 94 44 29 11 18 71 82 88 27 70 95 26 19 73 61 51 55 51\x0A195444  92 21 36 77 36 " \
      "27 25 45 48 16 73 90 71 53 47 39 75 33 96 11 22 18 15 48 20 16 90 50 66 11 49 91 23 60 81 53 57 18 19 40 54 " \
      "48\x0A233025  47 22 61 36 88 58 42 13 69 33 89 93 93 75 31 98 65 94 77 16 14 99 21 89 90 37 27 11 22 80 66 65 " \
      "31 70 76 29 49 92 51 38 27 47\x0A224202  69 33 97 97 51 59 15 17 92 59 84 19 33 54 78 15 50 28 40 68 75 23 55 " \
      "38 69 46 21 39 36 74 84 90 31 57 81 21 46 66 63 23 43 82\x0A246170  26 52 48 41 14 64 11 31 90 49 93 92 45 56 " \
      "99 85 81 26 34 27 55 55 85 26 41 83 41 46 89 41 66 96 92 16 47 73 59 85 57 88 70 49\x0A223337  26 74 51 31 10 " \
      "55 23 33 62 97 93 71 96 89 28 35 63 26 66 12 83 67 39 72 92 78 70 19 63 76 74 70 84 31 18 22 54 74 32 30 65 " \
      "15\x0A244180  88 20 28 71 54 74 73 90 12 35 49 94 69 20 18 88 80 88 73 65 19 40 23 17 21 48 71 89 96 61 92 81 " \
      "74 36 78 16 81 39 43 12 80 91\x0A241027  30 64 16 36 85 58 43 97 90 85 79 28 28 86 24 40 43 22 95 74 73 29 35 " \
      "13 82 67 77 76 19 70 29 61 92 51 82 98 40 83 72 33 81 41\x0A225646  55 16 69 49 35 88 71 14 64 16 23 34 81 89 " \
      "66 79 20 40 11 10 52 74 55 26 64 30 97 65 51 88 55 59 20 18 97 86 65 28 44 71 64 93\x0A217174  48 91 36 87 35 " \
      "11 40 67 90 25 39 85 29 97 57 44 99 88 34 83 75 10 73 63 44 63 56 17 94 16 28 78 55 63 19 22 37 36 42 16 49 " \
      "51\x0A222271  51 55 27 49 54 89 77 58 15 36 25 43 71 57 78 55 54 58 28 79 87 92 39 88 61 11 27 66 59 96 79 75 " \
      "69 25 16 40 68 30 16 12 51 48\x0A203973  71 29 57 59 30 75 67 39 95 14 48 49 35 93 56 94 14 59 12 49 19 40 16 " \
      "86 79 38 31 43 82 14 51 85 85 19 99 35 30 19 26 15 32 77 "

pre=pre.replace("\n"," ")     #处理数据：去除换行符
pre = pre.split(" ")         #处理数据：生成列表
s = Solver()                # 创建一个通用求解器
x = [Int('x%s'%i) for i in range(44)]   # 创建一个未知数列表x，里面包含x0~x43; x[1]==x1；创建44个是因为数据有偏移

'''
for i in range(44):
    print('int(pre[i*44+{}])*x[{}]+'.format(i,i),end="") #生成约束条件，怎么可能手敲！
'''
# 下面copy上生成出来的约束条件
for i in range(42):
    s.add(int(pre[i*44]) == int(pre[i*44+2])*x[2]+int(pre[i*44+3])*x[3]+int(pre[i*44+4])*x[4]+int(pre[i*44+5])*x[5]+int(pre[i*44+6])*x[6]+int(pre[i*44+7])*x[7]+int(pre[i*44+8])*x[8]+int(pre[i*44+9])*x[9]+int(pre[i*44+10])*x[10]+int(pre[i*44+11])*x[11]+int(pre[i*44+12])*x[12]+int(pre[i*44+13])*x[13]+int(pre[i*44+14])*x[14]+int(pre[i*44+15])*x[15]+int(pre[i*44+16])*x[16]+int(pre[i*44+17])*x[17]+int(pre[i*44+18])*x[18]+int(pre[i*44+19])*x[19]+int(pre[i*44+20])*x[20]+int(pre[i*44+21])*x[21]+int(pre[i*44+22])*x[22]+int(pre[i*44+23])*x[23]+int(pre[i*44+24])*x[24]+int(pre[i*44+25])*x[25]+int(pre[i*44+26])*x[26]+int(pre[i*44+27])*x[27]+int(pre[i*44+28])*x[28]+int(pre[i*44+29])*x[29]+int(pre[i*44+30])*x[30]+int(pre[i*44+31])*x[31]+int(pre[i*44+32])*x[32]+int(pre[i*44+33])*x[33]+int(pre[i*44+34])*x[34]+int(pre[i*44+35])*x[35]+int(pre[i*44+36])*x[36]+int(pre[i*44+37])*x[37]+int(pre[i*44+38])*x[38]+int(pre[i*44+39])*x[39]+int(pre[i*44+40])*x[40]+int(pre[i*44+41])*x[41]+int(pre[i*44+42])*x[42]+int(pre[i*44+43])*x[43])

print(s.check())  #.check() == unknow(无解)/sat(有解)
m=s.model()     #.model() 是每个未知数的解；
flag = []
for i in m:
    flag.append(str(m[i]))     #这里先转成str好处理，因为m[i]好像不是普通的‘int’型
for i in range(2,len(flag)+2):   #体现偏移；打印“flag”
      print(chr(int(str(m[x[i]]))),end="")   #按顺序遍历各个解；m[未知数变量名]==未知数变量的解，以此来顺序输出各个解的结果
                                             # 直接print(m) 可能是无序输出的解

#import z3
from z3 import *
# 关键就是求 ans = x^(x >>10) 里的x
# 常规方法还得自己写一个按位逆向的算法

ans = 0x6675FA7F228DBCEB6A2DC223A37FC64FE67E61

x = BitVec('x',160)      # 这里和普通的z3声明有区别，
                         # 意义为声明一个名为'x'的占160个bit的未知数变量
s= Solver()
s.add(x^(x >> 10)==ans)
print(s.check())
m = s.model()
print(m[x])