1、首先查壳,64位ELF无壳程序:
2、拖入IDA分析一下
2、D810去混淆
发现有一些无用的for循环,应该是使用了ollvm,所以使用D-810处理一下,D810下载地址:
所以咱们使用处理一下:Ctrl + Shift + T引用
首先从上面loaded一下ollvm.json,然后点击一下start会发现右边会变成绿色的loaded
然后咱们再看一下main函数,可以发现非常整洁,very nice好吧
前几个函数是使用RC4解密了一个ELF文件,所以我们在fclose之前给他动调截下来
我们发现在虚拟机里面,已经有了这个文件拿出来ida反编译一下
3、dump加密文件
可以看出来他是一个加密,翻到最后一个cmp对比,所以前面肯定是加密,所以咱们使用z3解一下,但是有些大佬是使用angr梭哈的,但是angr我还不会使用(太菜了),后面学习到了再来重温一下,目前就使用z3解一下
在这个文件中,有几个地方不好看,所以我重新给他处理了一下:
太乱了感觉,找不到循环条件(呜呜呜,我的代码功底太弱了)
v15=0
do{
v16=v15=0
v17=0
do{
v10=v17=0
v11,v12,v13=0
do{
v3=dword_2010[5*v15+v12] * v45[5*v12+1+v17]
v9=-105 * (39 * (2 * (v13 & v3) + (v13 ^ v3)) + 23) + 111
v4=v12++ ==4
v13=v9
}
while(!v4)
*v11=v9
v17++
}
while(v10!=4)
v15++
v14=0
}
while(v16!=4)
可以看到关键的加密就俩句
v3=dword_2010[5*v15+v12] * v45[5*v12+1+v17]
v9=-105 * (39 * (2 * (v13 & v3) + (v13 ^ v3)) + 23) + 111
所以就对这俩句放重点
这样可以使用python进行解了,下面还有一个异或得到值,所以异或一下就是密文
data1=[0x32, 0x44, 0xAA, 0x56, 0x63, 0x3D, 0x2B, 0x09, 0xCD, 0x34,
0x99, 0x3C, 0x56, 0xB8, 0x99, 0xDE, 0x26, 0x1F, 0x7E, 0x0B,
0x42, 0xC2, 0x1B, 0xEB, 0xF5]
data2=[0x44, 0x30, 0x5F, 0x79, 0x30, 0x75, 0x5F, 0x4C, 0x69, 0x6B,
0x65, 0x5F, 0x57, 0x68, 0x61, 0x74, 0x5F, 0x59, 0x6F, 0x75,
0x5F, 0x53, 0x65, 0x65, 0x3F]
enc=[0]*25
for i in range(len(data1)):
enc[i]=data1[i]^data2[i]
print(enc)
4、z3求解
下面就是进行z3求解,求出代码:
data1=[0x32, 0x44, 0xAA, 0x56, 0x63, 0x3D, 0x2B, 0x09, 0xCD, 0x34,
0x99, 0x3C, 0x56, 0xB8, 0x99, 0xDE, 0x26, 0x1F, 0x7E, 0x0B,
0x42, 0xC2, 0x1B, 0xEB, 0xF5]
data2=[0x44, 0x30, 0x5F, 0x79, 0x30, 0x75, 0x5F, 0x4C, 0x69, 0x6B,
0x65, 0x5F, 0x57, 0x68, 0x61, 0x74, 0x5F, 0x59, 0x6F, 0x75,
0x5F, 0x53, 0x65, 0x65, 0x3F]
enc=[0]*25
for i in range(len(data1)):
enc[i]=data1[i]^data2[i]
print(enc)
from z3 import *
x = Solver()
num=25
ans=[]
v20 = [BitVec(('%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
data3=[0]*25#此处就是得到的密文
dword=[0x00000000, 0xFFFFFFFE, 0xFFFFFFFF, 0x00000004, 0x00000001, 0xFFFFFFFF, 0x00000001, 0x00000000, 0x00000000, 0xFFFFFFFF, 0xFFFFFFFD, 0xFFFFFFFE, 0x00000000, 0xFFFFFFF6, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFE, 0x00000001, 0xFFFFFFF3, 0xFFFFFFFF, 0xFFFFFFFA, 0xFFFFFFFF, 0xFFFFFFFE, 0x00000001, 0xFFFFFFFE, 0x00000000, 0x00000000, 0x00000000]
for i in range(5):
for j in range(5):
v13 = 0
for k in range(5):
v3=((dword[5*i+k])*v20[5*k+j])&0xff
v9 = (-105 * (39 * (2 * (v13 & v3) + (v13 ^ v3)) + 23) + 111)&0xff
v13 = v9
data3[5*i+j]=v13
for i in range(25):
x.add(data3[i]==enc[i])
x.check()
flag=''
result = x.model()
print(result)
参考一下上面的代码,然后得到的result的前面的数字大小排序得到flag
根据上面的result输出flag:
data = {
20: 115,
18: 101,
24: 125,
2: 67,
12: 83,
17: 95,
10: 95,
3: 84,
21: 121,
15: 115,
23: 104,
13: 115,
7: 72,
16: 64,
5: 123,
14: 95,
22: 104,
9: 116,
6: 84,
11: 49,
1: 75,
19: 65,
8: 117,
0: 78,
4: 70
}
# 按照键排序
sorted_keys = sorted(data.keys())
# 输出排序后的字符
for key in sorted_keys:
flag+=chr(data[key])
print(flag)
得到flag是:NKCTF{THut_1Ss_s@_eAsyhh}
此题收获到了ollvm的简单去混淆,还有z3的简单使用,向大佬学习