【WKCTF】so_easy

用压缩包打开apk，把里面的x86_64的 .so文件解压出来拖入ida

so_main.png

有两种方法，一个是z3爆破，一个是根据这个魔改CRC进行逆向

CRC校验

先说正版做法CRC逆向

【[CRC校验]手算与直观演示】 https://www.bilibili.com/video/BV1V4411Z7VA/?share_source=copy_web&vd_source=86d6e63e560e68bb720088caa831e036

【CRC原理】https://bbs.21ic.com/icview-2403118-1-2.html?_dsign=e20cd6df

【上面 CRC原理 看不懂先看这个】https://blog.csdn.net/eydwyz/article/details/105705831?ops_request_misc=%257B%2522request%255Fid%2522%253A%2522172121223216800182199332%2522%252C%2522scm%2522%253A%252220140713.130102334.pc%255Fall.%2522%257D&request_id=172121223216800182199332&biz_id=0&utm_medium=distribute.pc_search_result.none-task-blog-2~all~first_rank_ecpm_v1~rank_v31_ecpm-20-105705831-null-null.142

找一个脚本CRC32的脚本，把相应的数据修改过来

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
#include <stdio.h>
int main(void)
{
	unsigned char s[] = {-82, -127, -70, -63, -16, -107, 10, 84, 20, 3,
	74, -30, 82, 78, -124, -8, -55, 62, 20, -104, -113, -104, -3, 9, 94, -83, 5,
	-76, 1, 15, -64, 63};
	__int64 *ans = NULL;
	int i = 0, j = 0;
	for(i = 0; i < 32; i += 8)
	{
		for(j = 0; j < 255; j++)
		{
			ans = (__int64 *)(s+i);
			if(*ans & 1)							//判断是否为奇数 ，因为CRC加密后的末位就是1，所以这里异或没问题
		  	{
				if(*ans < 0)						//奇数小于0的情况
				{
					*ans ^= 0x71234EA7D92996F5;
					*ans /= 2;
				}
				else								//奇数大于0的情况，需要进行将补偿性异或，保证为负数（不知道为啥）
				{
					*ans ^= 0x71234EA7D92996F5;
					*ans /= 2;
					*ans ^= 0x8000000000000000;
				}
			}
			else									//不是奇数的情况，因为CRC异或完应为奇数，所以偶数直接进行右移操作
			{
				if(*ans < 0)						//偶数小于0的情况，需要进行将补偿性异或，保证为负数（不知道为啥）
				{
					*ans /= 2;
					*ans ^= 0x8000000000000000;
				}
				else								//偶数大于0的情况
				{
					*ans /= 2;
				}
			}
		}
	}
	for(j = 0; j < 32; j++){
		printf("%c", s[j]);
	}
		
	return 0;
}

Z3爆破

然后就是比较无脑的爆破脚本

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
from z3 import *

final_flag=''

enc = [0x540A95F0C1BA81AE, 0xF8844E52E24A0314, 0x09FD988F98143EC9, 0x3FC00F01B405AD5E]

xor_value = BitVecVal(0x71234EA7D92996F5, 64)

flag = BitVec('flag', 64)

v11=255
# 创建求解器
s = Solver()
temp = flag
for _ in range(v11,0,-5):
    v12 = (2 * temp) ^ xor_value
    v12 = If(temp >= 0, 2 * temp, v12)
    
    v13 = (2 * v12) ^ xor_value
    v13 = If(v12 >= 0, 2 * v12, v13)
    
    v14 = (2 * v13) ^ xor_value
    v14 = If(v13 >= 0, 2 * v13, v14)
    
    v15 = (2 * v14) ^ xor_value
    v15 = If(v14 >= 0, 2 * v14, v15)
    
    temp = (2 * v15) ^ xor_value
    temp = If(v15 >= 0, 2 * v15, temp)



s.add(temp==enc[0])

# 检查是否有解
if s.check() == sat:
    # 如果有解，打印模型
    m = s.model()
    flag_value = m[flag].as_long()
    flag_str = hex(flag_value)
    # 去除前缀 '0x'，得到纯十六进制字符串
    hex_str_without_prefix = flag_str[2:]
    byte_str = bytes.fromhex(hex_str_without_prefix)
    decoded_str = byte_str.decode('utf-8') 
    final_flag+=decoded_str[::-1]
else:
    print("No solution exists")



flag = BitVec('flag', 64)

v11=255
# 创建求解器
s = Solver()
temp = flag
for _ in range(v11,0,-5):
    v12 = (2 * temp) ^ xor_value
    v12 = If(temp >= 0, 2 * temp, v12)
    
    v13 = (2 * v12) ^ xor_value
    v13 = If(v12 >= 0, 2 * v12, v13)
    
    v14 = (2 * v13) ^ xor_value
    v14 = If(v13 >= 0, 2 * v13, v14)
    
    v15 = (2 * v14) ^ xor_value
    v15 = If(v14 >= 0, 2 * v14, v15)
    
    temp = (2 * v15) ^ xor_value
    temp = If(v15 >= 0, 2 * v15, temp)



s.add(temp==enc[1])

# 检查是否有解
if s.check() == sat:
    # 如果有解，打印模型
    m = s.model()
    flag_value = m[flag].as_long()
    flag_str = hex(flag_value)
    # 去除前缀 '0x'，得到纯十六进制字符串
    hex_str_without_prefix = flag_str[2:]
    byte_str = bytes.fromhex(hex_str_without_prefix)
    decoded_str = byte_str.decode('utf-8') 
    final_flag+=decoded_str[::-1]
else:
    print("No solution exists")

flag = BitVec('flag', 64)

v11=255
# 创建求解器
s = Solver()
temp = flag
for _ in range(v11,0,-5):
    v12 = (2 * temp) ^ xor_value
    v12 = If(temp >= 0, 2 * temp, v12)
    
    v13 = (2 * v12) ^ xor_value
    v13 = If(v12 >= 0, 2 * v12, v13)
    
    v14 = (2 * v13) ^ xor_value
    v14 = If(v13 >= 0, 2 * v13, v14)
    
    v15 = (2 * v14) ^ xor_value
    v15 = If(v14 >= 0, 2 * v14, v15)
    
    temp = (2 * v15) ^ xor_value
    temp = If(v15 >= 0, 2 * v15, temp)



s.add(temp==enc[2])

# 检查是否有解
if s.check() == sat:
    # 如果有解，打印模型
    m = s.model()
    flag_value = m[flag].as_long()
    flag_str = hex(flag_value)
    # 去除前缀 '0x'，得到纯十六进制字符串
    hex_str_without_prefix = flag_str[2:]
    byte_str = bytes.fromhex(hex_str_without_prefix)
    decoded_str = byte_str.decode('utf-8') 
    final_flag+=decoded_str[::-1]
else:
    print("No solution exists")


flag = BitVec('flag', 64)

v11=255
# 创建求解器
s = Solver()
temp = flag
for _ in range(v11,0,-5):
    v12 = (2 * temp) ^ xor_value
    v12 = If(temp >= 0, 2 * temp, v12)
    
    v13 = (2 * v12) ^ xor_value
    v13 = If(v12 >= 0, 2 * v12, v13)
    
    v14 = (2 * v13) ^ xor_value
    v14 = If(v13 >= 0, 2 * v13, v14)
    
    v15 = (2 * v14) ^ xor_value
    v15 = If(v14 >= 0, 2 * v14, v15)
    
    temp = (2 * v15) ^ xor_value
    temp = If(v15 >= 0, 2 * v15, temp)



s.add(temp==enc[3])

# 检查是否有解
if s.check() == sat:
    # 如果有解，打印模型
    m = s.model()
    flag_value = m[flag].as_long()
    flag_str = hex(flag_value)
    # 去除前缀 '0x'，得到纯十六进制字符串
    hex_str_without_prefix = flag_str[2:]
    byte_str = bytes.fromhex(hex_str_without_prefix)
    decoded_str = byte_str.decode('utf-8') 
    final_flag+=decoded_str[::-1]
else:
    print("No solution exists")


print(final_flag)

比较考验Z3约束器的使用