IDA分析程序:
应该是直接通过Linux进行./outputfile 得到文件分析:
先是一大堆的变量赋值,然后是一大堆的ollvm的混淆的算式
之后再进行的是
一个类似于矩阵加密的过程
最后是一个异或操作
整理思路:
先是进行的是变量赋值,然后是进行的算式加减异或以及位运算,然后是矩阵加密,最后的结果与异或之后的结果进行比较
- 全正向爆破:
我们通过z3进行变量赋值,然后经过同样的算式运算,之后进行同样的矩阵加密,得到这一大串加密过程去相等于enc
类似于(-105 * (39 * (v44[0] + -105 * (39 * (v33 + -105 * (39 * (v34 + 3) + 23) + 111) + 23) + 111) + 23) + 111)+矩阵加密==enc[i]
这里我们看看laogong的wp
`#!/usr/bin/env python3
'''
from Crypto.Cipher import ARC4
data = open('./REEZ', 'rb').read()[0x3070: 0x3070 + 0x3F50]
data = ARC4.new(b'do_you_like_what_you_see?').decrypt(data)
open('out', 'wb').write(data)
'''
from z3 import *
s = Solver()
x = [BitVec('x%d' % i, 8) for i in range(25)]
for i in x:
s.add(i > 0)
s.add(i < 0x7f)
input_inv = x[::-1]
input_inv[24] = -105 * (39 * (2 * (input_inv[24] & (-105 * (39 * (2 * (input_inv[13] & (-105 * (39 * (2 * (input_inv[14] & 3) + (input_inv[14] ^ 3)) + 23) + 111)) + (input_inv[13] ^ (-105 * (39 * (2 * (input_inv[14] & 3) + (input_inv[14] ^ 3)) + 23) + 111))) + 23) + 111)) + (input_inv[24] ^ (-105 * (39 * (2 * (input_inv[13] & (-105 * (39 * (2 * (input_inv[14] & 3) + (input_inv[14] ^ 3)) + 23) + 111)) + (input_inv[13] ^ (-105 * (39 * (2 * (input_inv[14] & 3) + (input_inv[14] ^ 3)) + 23) + 111))) + 23) + 111))) + 23) + 111
input_inv[23] = -105* (39* (2 * ((input_inv[11] ^ input_inv[10]) & input_inv[23])+ (input_inv[11] ^ input_inv[10] ^ input_inv[23]))+ 23)+ 111;
input_inv[22] = -105* (39* (2* (input_inv[22] & (-105* (39 * (2 * (input_inv[10] & input_inv[9]) + (input_inv[10] ^ input_inv[9])) + 23)+ 111))+ (input_inv[22] ^ (-105* (39 * (2 * (input_inv[10] & input_inv[9]) + (input_inv[10] ^ input_inv[9])) + 23)+ 111)))+ 23)+ 111;
input_inv[21] = -105* (39 * (2 * ((input_inv[7] ^ 0x17) & input_inv[21]) + (input_inv[7] ^ 0x17 ^ input_inv[21])) + 23)+ 111;
input_inv[20] = -105* (39* (2* (input_inv[20] & (-105* (39 * (2 * (input_inv[4] & (-105 * (39 * (2 * (input_inv[15] & 0xFB) + (input_inv[15] ^ 0xFB)) + 23) + 111)) + (input_inv[4] ^ (-105 * (39 * (2 * (input_inv[15] & 0xFB) + (input_inv[15] ^ 0xFB)) + 23) + 111))) + 23)+ 111))+ (input_inv[20] ^ (-105* (39 * (2 * (input_inv[4] & (-105 * (39 * (2 * (input_inv[15] & 0xFB) + (input_inv[15] ^ 0xFB)) + 23) + 111)) + (input_inv[4] ^ (-105 * (39 * (2 * (input_inv[15] & 0xFB) + (input_inv[15] ^ 0xFB)) + 23) + 111))) + 23)+ 111)))+ 23)+ 111;
input_inv[19] = -105* (39* (2 * (input_inv[19] & (~input_inv[1] + input_inv[3] + 1))+ (input_inv[19] ^ (~input_inv[1] + input_inv[3] + 1)))+ 23)+ 111;
input_inv[18] = -105* (39* (2* (input_inv[18] & (-105* (39 * (2 * (input_inv[16] & input_inv[17]) + (input_inv[16] ^ input_inv[17])) + 23)+ 111))+ (input_inv[18] ^ (-105* (39 * (2 * (input_inv[16] & input_inv[17]) + (input_inv[16] ^ input_inv[17])) + 23)+ 111)))+ 23)+ 111;
input_inv[17] = -105* (39* (2* (input_inv[17] & (-105* (39 * (2 * ((~input_inv[4] + input_inv[1] + 1) & 0x11) + ((~input_inv[4] + input_inv[1] + 1) ^ 0x11)) + 23)+ 111))+ (input_inv[17] ^ (-105* (39 * (2 * ((~input_inv[4] + input_inv[1] + 1) & 0x11) + ((~input_inv[4] + input_inv[1] + 1) ^ 0x11)) + 23)+ 111)))+ 23)+ 111;
input_inv[16] = -105* (39* (2* (input_inv[16] & (input_inv[5] ^ (-105 * (39 * (2 * (input_inv[6] & 1) + (input_inv[6] ^ 1)) + 23)+ 111)))+ (input_inv[16] ^ input_inv[5] ^ (-105 * (39 * (2 * (input_inv[6] & 1) + (input_inv[6] ^ 1)) + 23) + 111)))+ 23)+ 111;
input_inv[15] = ~input_inv[8]+ -105 * (39 * (2 * (input_inv[7] & input_inv[15]) + (input_inv[7] ^ input_inv[15])) + 23)+ 111+ 1;
input_inv[14] = -105* (39* (2* (input_inv[14] & (-105* (39 * (2 * (input_inv[10] & input_inv[9]) + (input_inv[10] ^ input_inv[9])) + 23)+ 111))+ (input_inv[14] ^ (-105* (39 * (2 * (input_inv[10] & input_inv[9]) + (input_inv[10] ^ input_inv[9])) + 23)+ 111)))+ 23)+ 111;
input_inv[13] = -105* (39* (2* (input_inv[12] & (-105* (39 * (2 * (input_inv[11] & (-105* (39 * (2 * (input_inv[13] & 0xF9) + (input_inv[13] ^ 0xF9)) + 23)+ 111)) + (input_inv[11] ^ (-105* (39 * (2 * (input_inv[13] & 0xF9) + (input_inv[13] ^ 0xF9)) + 23)+ 111))) + 23)+ 111))+ (input_inv[12] ^ (-105* (39 * (2 * (input_inv[11] & (-105* (39 * (2 * (input_inv[13] & 0xF9) + (input_inv[13] ^ 0xF9)) + 23)+ 111)) + (input_inv[11] ^ (-105* (39 * (2 * (input_inv[13] & 0xF9) + (input_inv[13] ^ 0xF9)) + 23)+ 111))) + 23)+ 111)))+ 23)+ 111;
input_inv[12] = -105 * (39 * (2 * (input_inv[12] & input_inv[13]) + (input_inv[12] ^ input_inv[13])) + 23) + 111;
input_inv[11] = -105* (39* (2 * (input_inv[11] & (input_inv[17] ^ input_inv[16]))+ (input_inv[11] ^ input_inv[17] ^ input_inv[16]))+ 23)+ 111;
input_inv[10] = -105* (39* (2* (input_inv[19] & (-105* (39 * (2 * (input_inv[20] & (-105* (39 * (2 * (input_inv[10] & 0xC) + (input_inv[10] ^ 0xC)) + 23)+ 111)) + (input_inv[20] ^ (-105* (39 * (2 * (input_inv[10] & 0xC) + (input_inv[10] ^ 0xC)) + 23)+ 111))) + 23)+ 111))+ (input_inv[19] ^ (-105* (39 * (2 * (input_inv[20] & (-105* (39 * (2 * (input_inv[10] & 0xC) + (input_inv[10] ^ 0xC)) + 23)+ 111)) + (input_inv[20] ^ (-105* (39 * (2 * (input_inv[10] & 0xC) + (input_inv[10] ^ 0xC)) + 23)+ 111))) + 23)+ 111)))+ 23)+ 111;
input_inv[9] = -105* (39* (2 * (input_inv[21] & (-105 * (39 * (2 * (input_inv[9] & 8) + (input_inv[9] ^ 8)) + 23) + 111))+ (input_inv[21] ^ (-105 * (39 * (2 * (input_inv[9] & 8) + (input_inv[9] ^ 8)) + 23) + 111)))+ 23)+ 111;
input_inv[8] = -105* (39 * (2 * ((input_inv[22] ^ 0x4D) & input_inv[8]) + (input_inv[22] ^ 0x4D ^ input_inv[8])) + 23)+ 111;
input_inv[7] = -105* (39* (2* (input_inv[7] & (-105 * (39 * (2 * ((input_inv[23] ^ 0x17) & 0xF9) + (input_inv[23] ^ 0xEE)) + 23) + 111))+ (input_inv[7] ^ (-105 * (39 * (2 * ((input_inv[23] ^ 0x17) & 0xF9) + (input_inv[23] ^ 0xEE)) + 23) + 111)))+ 23)+ 111;
input_inv[6] = -105* (39* (2 * ((input_inv[7] ^ input_inv[9]) & input_inv[6]) + (input_inv[7] ^ input_inv[9] ^ input_inv[6]))+ 23)+ 111;
input_inv[5] = -105* (39* (2* (input_inv[12] & (-105 * (39 * (2 * (input_inv[10] & input_inv[5]) + (input_inv[10] ^ input_inv[5])) + 23) + 111))+ (input_inv[12] ^ (-105 * (39 * (2 * (input_inv[10] & input_inv[5]) + (input_inv[10] ^ input_inv[5])) + 23) + 111)))+ 23)+ 111;
input_inv[4] = -105 * (39 * (2 * (input_inv[4] & input_inv[13]) + (input_inv[4] ^ input_inv[13])) + 23) + 111;
input_inv[3] = -105* (39* (2* (input_inv[16] & (-105 * (39 * (2 * (input_inv[3] & input_inv[18]) + (input_inv[3] ^ input_inv[18])) + 23) + 111))+ (input_inv[16] ^ (-105 * (39 * (2 * (input_inv[3] & input_inv[18]) + (input_inv[3] ^ input_inv[18])) + 23) + 111)))+ 23)+ 111;
input_inv[2] = -105 * (39 * (2 * (input_inv[19] & input_inv[2]) + (input_inv[19] ^ input_inv[2])) + 23) + 111;
input_inv[1] = -105* (39* (2 * ((input_inv[24] ^ input_inv[22]) & input_inv[1]) + (input_inv[24] ^ input_inv[22] ^ input_inv[1]))+ 23)+ 111;
input_inv[0] = -105* (39* (2 * (input_inv[0] & (-105 * (39 * (2 * (input_inv[23] & 0x18) + (input_inv[23] ^ 0x18)) + 23) + 111))+ (input_inv[0] ^ (-105 * (39 * (2 * (input_inv[23] & 0x18) + (input_inv[23] ^ 0x18)) + 23) + 111)))+ 23)+ 111;
input_inv = input_inv[::-1]
dword_2010 = [0, -2, -1, 4, 1, -1, 1, 0, 0, -1, -3, -2, 0, -0xA, -1, -1, -2, 1, -0xD, -1, -6, -1, -2, 1, -2]
out = [0] * 25
for a in range(5):
for b in range(5):
v13 = 0
for c in range(5):
v3 = dword_2010[5 * a + c] * input_inv[5 * c + b]
v13 = -105 * (39 * (2 * (v13 & v3) + (v13 ^ v3)) + 23) + 111
out[5 * a + b] = v13
result1 = bytes.fromhex('3244AA56633D2B09CD34993C56B899DE261F7E0B42C21BEBF5')
result2 = b'D0_y0u_Like_What_You_See?'
for i in range(25):
s.add(out[i] == result1[i] ^ result2[i])
assert s.check() == sat
model = s.model()
flag = bytes([model[i].as_long() for i in x])
print(flag)
NKCTF{THut_1Ss_s@_eAsyhh}`
半正向半逆向
我们先去逆向结果,首先是进行的是异或操作,然后是去逆矩阵操作,我们用结果去乘以逆矩阵,得到半逆向的结果
再着,我们正向进行,先变量赋值,然后进行大堆算式的赋值,让算式的结果来等于我们半逆向的结果进行z3爆破
得到结果
半逆向:
通过矩阵计算器 - Reshish来获取逆矩阵的结果
`from z3 import *
x = Solver()
num=25
ans=[]
v20 = [BitVec(('v20[%d]' % i),8) for i in range(25)]
v45=v20[0]
v44=v20[1]
v43=v20[2]
v42=v20[3]
v41=v20[4]
v40=v20[5]
v39=v20[6]
v38=v20[7]
v37=v20[8]
v36=v20[9]
v35=v20[10]
v34=v20[11]
v33=v20[12]
v32=v20[13]
v31=v20[14]
v30=v20[15]
v29=v20[16]
v28=v20[17]
v27=v20[18]
v26=v20[19]
v25=v20[20]
v24=v20[21]
v23=v20[22]
v22=v20[23]
v21=v20[24]
v45 = -105* (39* (2* (v45 & (-105* (39* (2 * (v34 & (-105 * (39 * (2 * (v35 & 3) + (v35 ^ 3)) + 23) + 111))+ (v34 ^ (-105 * (39 * (2 * (v35 & 3) + (v35 ^ 3)) + 23) + 111)))+ 23)+ 111))+ (v45 ^ (-105* (39* (2 * (v34 & (-105 * (39 * (2 * (v35 & 3) + (v35 ^ 3)) + 23) + 111))
+ (v34 ^ (-105 * (39 * (2 * (v35 & 3) + (v35 ^ 3)) + 23) + 111)))
+ 23)
+ 111)))
+ 23)+ 111
v44 = -105 * (39 * (2 * ((v32 ^ v31) & v44) + (v32 ^ v31 ^ v44)) + 23) + 111
v43 = -105* (39
* (2 * (v43 & (-105 * (39 * (2 * (v31 & v30) + (v31 ^ v30)) + 23) + 111))
+ (v43 ^ (-105 * (39 * (2 * (v31 & v30) + (v31 ^ v30)) + 23) + 111)))
+ 23)+ 111
v42 = -105 * (39 * (2 * ((v28 ^ 0x17) & v42) + (v28 ^ 0x17 ^ v42)) + 23) + 111
v41 = -105* (39
* (2
* (v41 & (-105
* (39
* (2 * (v25 & (-105 * (39 * (2 * (v36 & 0xFB) + (v36 ^ 0xFB)) + 23) + 111))
+ (v25 ^ (-105 * (39 * (2 * (v36 & 0xFB) + (v36 ^ 0xFB)) + 23) + 111)))
+ 23)
+ 111))
+ (v41 ^ (-105
* (39
* (2 * (v25 & (-105 * (39 * (2 * (v36 & 0xFB) + (v36 ^ 0xFB)) + 23) + 111))
+ (v25 ^ (-105 * (39 * (2 * (v36 & 0xFB) + (v36 ^ 0xFB)) + 23) + 111)))
+ 23)
+ 111)))
+ 23)+ 111
v40 = -105 * (39 * (2 * (v40 & (~v22 + v24 + 1)) + (v40 ^ (~v22 + v24 + 1))) + 23) + 111
v39 = -105* (39
* (2 * (v39 & (-105 * (39 * (2 * (v37 & v38) + (v37 ^ v38)) + 23) + 111))
+ (v39 ^ (-105 * (39 * (2 * (v37 & v38) + (v37 ^ v38)) + 23) + 111)))
+ 23)+ 111
v38 = -105* (39
* (2 * (v38 & (-105 * (39 * (2 * ((~v25 + v22 + 1) & 0x11) + ((~v25 + v22 + 1) ^ 0x11)) + 23) + 111))
+ (v38 ^ (-105 * (39 * (2 * ((~v25 + v22 + 1) & 0x11) + ((~v25 + v22 + 1) ^ 0x11)) + 23) + 111)))
+ 23)+ 111
v37 = -105* (39
* (2 * (v37 & (v26 ^ (-105 * (39 * (2 * (v27 & 1) + (v27 ^ 1)) + 23) + 111)))
+ (v37 ^ v26 ^ (-105 * (39 * (2 * (v27 & 1) + (v27 ^ 1)) + 23) + 111)))
+ 23)+ 111
v36 = ~v29 + -105 * (39 * (2 * (v28 & v36) + (v28 ^ v36)) + 23) + 111 + 1
v35 = -105* (39
* (2 * (v35 & (-105 * (39 * (2 * (v31 & v30) + (v31 ^ v30)) + 23) + 111))
+ (v35 ^ (-105 * (39 * (2 * (v31 & v30) + (v31 ^ v30)) + 23) + 111)))
+ 23)+ 111
v34 = -105* (39
* (2
* (v33 & (-105
* (39
* (2 * (v32 & (-105 * (39 * (2 * (v34 & 0xF9) + (v34 ^ 0xF9)) + 23) + 111))
+ (v32 ^ (-105 * (39 * (2 * (v34 & 0xF9) + (v34 ^ 0xF9)) + 23) + 111)))
+ 23)
+ 111))
+ (v33 ^ (-105
* (39
* (2 * (v32 & (-105 * (39 * (2 * (v34 & 0xF9) + (v34 ^ 0xF9)) + 23) + 111))
+ (v32 ^ (-105 * (39 * (2 * (v34 & 0xF9) + (v34 ^ 0xF9)) + 23) + 111)))
+ 23)
+ 111)))
+ 23)+ 111
v33 = -105 * (39 * (2 * (v33 & v34) + (v33 ^ v34)) + 23) + 111
v32 = -105 * (39 * (2 * (v32 & (v38 ^ v37)) + (v32 ^ v38 ^ v37)) + 23) + 111
v31 = -105* (39
* (2
* (v40 & (-105
* (39
* (2 * (v41 & (-105 * (39 * (2 * (v31 & 0xC) + (v31 ^ 0xC)) + 23) + 111))
+ (v41 ^ (-105 * (39 * (2 * (v31 & 0xC) + (v31 ^ 0xC)) + 23) + 111)))
+ 23)
+ 111))
+ (v40 ^ (-105
* (39
* (2 * (v41 & (-105 * (39 * (2 * (v31 & 0xC) + (v31 ^ 0xC)) + 23) + 111))
+ (v41 ^ (-105 * (39 * (2 * (v31 & 0xC) + (v31 ^ 0xC)) + 23) + 111)))
+ 23)
+ 111)))
+ 23)+ 111
v30 = -105* (39
* (2 * (v42 & (-105 * (39 * (2 * (v30 & 8) + (v30 ^ 8)) + 23) + 111))
+ (v42 ^ (-105 * (39 * (2 * (v30 & 8) + (v30 ^ 8)) + 23) + 111)))
+ 23)+ 111
v29 = -105 * (39 * (2 * ((v43 ^ 0x4D) & v29) + (v43 ^ 0x4D ^ v29)) + 23) + 111
v28 = -105* (39
* (2 * (v28 & (-105 * (39 * (2 * ((v44 ^ 0x17) & 0xF9) + (v44 ^ 0xEE)) + 23) + 111))
+ (v28 ^ (-105 * (39 * (2 * ((v44 ^ 0x17) & 0xF9) + (v44 ^ 0xEE)) + 23) + 111)))
+ 23)+ 111
v27 = -105 * (39 * (2 * ((v28 ^ v30) & v27) + (v28 ^ v30 ^ v27)) + 23) + 111
v26 = -105* (39
* (2 * (v33 & (-105 * (39 * (2 * (v31 & v26) + (v31 ^ v26)) + 23) + 111))
+ (v33 ^ (-105 * (39 * (2 * (v31 & v26) + (v31 ^ v26)) + 23) + 111)))
+ 23)+ 111
v25 = -105 * (39 * (2 * (v25 & v34) + (v25 ^ v34)) + 23) + 111
v24 = -105* (39
* (2 * (v37 & (-105 * (39 * (2 * (v24 & v39) + (v24 ^ v39)) + 23) + 111))
+ (v37 ^ (-105 * (39 * (2 * (v24 & v39) + (v24 ^ v39)) + 23) + 111)))
+ 23)+ 111
v23 = -105 * (39 * (2 * (v40 & v23) + (v40 ^ v23)) + 23) + 111
v22 = -105 * (39 * (2 * ((v45 ^ v43) & v22) + (v45 ^ v43 ^ v22)) + 23) + 111
v21 = -105* (39
* (2 * (v21 & (-105 * (39 * (2 * (v44 & 0x18) + (v44 ^ 0x18)) + 23) + 111))
+ (v21 ^ (-105 * (39 * (2 * (v44 & 0x18) + (v44 ^ 0x18)) + 23) + 111)))
+ 23)+ 111
v20[0]=v45
v20[1]=v44
v20[2]=v43
v20[3]=v42
v20[4]=v41
v20[5]=v40
v20[6]=v39
v20[7]=v38
v20[8]=v37
v20[9]=v36
v20[10]=v35
v20[11]=v34
v20[12]=v33
v20[13]=v32
v20[14]=v31
v20[15]=v30
v20[16]=v29
v20[17]=v28
v20[18]=v27
v20[19]=v26
v20[20]=v25
v20[21]=v24
v20[22]=v23
v20[23]=v22
v20[24]=v21
for i in range(25):
v20[i]&=0xff
rev = [-31, 119, 21, -100, 40,
-116, 17, 78, -100, -109,
49, -16, 67, 69, 31,
23, -104, -72, 20, -93,
99, 38, -12, 92, 12]
for i in range(25):
x.add(v20[i]==rev[i])
if x.check() == sat:
model = x.model()
print(model)
v20[21] = 121
v20[15] = 115
v20[11] = 49
v20[20] = 115
v20[7] = 72
v20[18] = 101
v20[2] = 67
v20[23] = 104
v20[16] = 64
v20[12] = 83
v20[22] = 104
v20[14] = 95
v20[0] = 78
v20[10] = 95
v20[4] = 70
v20[13] = 115
v20[9] = 116
v20[19] = 65
v20[3] = 84
v20[17] = 95
v20[1] = 75
v20[5] = 123
v20[6] = 84
v20[24] = 125
v20[8] = 117
flag = ''
for i in range(25):
flag += chr(v20[i])
print(flag)