HGAME 2024网络攻防大赛—week4部分题目题解
reverse
change
IDA打开，又是一个cpp程序
先看一下main函数
先赋值一个字符串am2qasl给v10，后读入flag，经过sub_1400029A0函数的加密，最后和密文byte_140008000比较，逻辑很清晰，进入sub_1400029A0函数看看
加密就是在奇偶位调用不同的异或，为奇则a2 ^ a1，为偶则(a2 ^ a1) + 10
这里的a1，a2应该分别就是flag和上面的字符串am2qasl
exp：
1
2
3
4
5
6
7
8
9
| v = [0x13, 0x0A, 0x5D, 0x1C, 0x0E, 0x08, 0x23, 0x06, 0x0B, 0x4B,
0x38, 0x22, 0x0D, 0x1C, 0x48, 0x0C, 0x66, 0x15, 0x48, 0x1B,
0x0D, 0x0E, 0x10, 0x4F]
s = "am2qasl"
for i in range(len(v)):
if i % 2 == 0:
print(chr(ord(s[i % 7]) ^ (v[i] - 10)), end='')
else:
print(chr(ord(s[i % 7]) ^ (v[i])), end='')
|
again!
是python逆向，首先先对exe解包，拿到pyc文件
但是发现pyc文件无法反编译，这个时候需要通过查看字节码来知道程序的逻辑
使用如下脚本查看字节码
1
2
3
4
| import dis,marshal
f=open("bin1.pyc", "rb").read()
code=marshal.loads(f[16:])
dis.dis(code)
|
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
| 0 0 RESUME 0
1 2 LOAD_CONST 0 (0)
4 LOAD_CONST 1 (None)
6 IMPORT_NAME 0 (hashlib)
8 STORE_NAME 0 (hashlib)
2 10 PUSH_NULL
12 LOAD_NAME 1 (print)
14 LOAD_CONST 2 ('you should use this execute file to decrypt "bin2"')
16 PRECALL 1
20 CALL 1
30 POP_TOP
3 32 PUSH_NULL
34 LOAD_NAME 1 (print)
36 LOAD_CONST 3 ('hint:md5')
38 PRECALL 1
42 CALL 1
52 POP_TOP
4 54 PUSH_NULL
56 LOAD_NAME 2 (bytearray)
58 PRECALL 0
62 CALL 0
72 STORE_NAME 3 (s)
5 74 PUSH_NULL
76 LOAD_NAME 2 (bytearray)
78 PUSH_NULL
80 LOAD_NAME 4 (open)
82 LOAD_CONST 4 ('bin1.pyc')
84 LOAD_CONST 5 ('rb')
86 PRECALL 2
90 CALL 2
100 LOAD_METHOD 5 (read)
122 PRECALL 0
126 CALL 0
136 PRECALL 1
140 CALL 1
150 STORE_NAME 6 (f)
6 152 LOAD_CONST 6 ('jkasnwojasd')
154 STORE_NAME 7 (t)
8 156 PUSH_NULL
158 LOAD_NAME 8 (range)
160 LOAD_CONST 0 (0)
162 LOAD_CONST 7 (15)
164 PRECALL 2
168 CALL 2
178 GET_ITER
>> 180 FOR_ITER 106 (to 394)
182 STORE_NAME 9 (i)
9 184 LOAD_NAME 6 (f)
186 LOAD_NAME 9 (i)
188 BINARY_SUBSCR
198 LOAD_NAME 6 (f)
200 LOAD_NAME 9 (i)
202 LOAD_CONST 8 (6)
204 BINARY_OP 6 (%)
208 BINARY_SUBSCR
218 BINARY_OP 0 (+)
222 PUSH_NULL
224 LOAD_NAME 10 (ord)
226 LOAD_NAME 7 (t)
228 LOAD_NAME 9 (i)
230 LOAD_CONST 8 (6)
232 BINARY_OP 6 (%)
236 BINARY_SUBSCR
246 PRECALL 1
250 CALL 1
260 PUSH_NULL
262 LOAD_NAME 10 (ord)
264 LOAD_NAME 7 (t)
266 LOAD_NAME 9 (i)
268 PUSH_NULL
270 LOAD_NAME 11 (len)
272 LOAD_NAME 7 (t)
274 PRECALL 1
278 CALL 1
288 BINARY_OP 6 (%)
292 BINARY_SUBSCR
302 PRECALL 1
306 CALL 1
316 BINARY_OP 0 (+)
320 BINARY_OP 12 (^)
324 LOAD_CONST 9 (256)
326 BINARY_OP 6 (%)
330 LOAD_NAME 6 (f)
332 LOAD_NAME 9 (i)
334 STORE_SUBSCR
10 338 LOAD_NAME 3 (s)
340 LOAD_METHOD 12 (append)
362 LOAD_NAME 6 (f)
364 LOAD_NAME 9 (i)
366 BINARY_SUBSCR
376 PRECALL 1
380 CALL 1
390 POP_TOP
392 JUMP_BACKWARD 107 (to 180)
12 >> 394 PUSH_NULL
396 LOAD_NAME 1 (print)
398 LOAD_NAME 3 (s)
400 PRECALL 1
404 CALL 1
414 POP_TOP
13 416 PUSH_NULL
418 LOAD_NAME 0 (hashlib)
420 LOAD_ATTR 13 (md5)
430 PUSH_NULL
432 LOAD_NAME 14 (bytes)
434 LOAD_NAME 3 (s)
436 PRECALL 1
440 CALL 1
450 PRECALL 1
454 CALL 1
464 LOAD_METHOD 15 (hexdigest)
486 PRECALL 0
490 CALL 0
500 STORE_NAME 16 (md5_hash)
502 LOAD_CONST 1 (None)
504 RETURN_VALUE
|
这段字节码经过翻译后如下所示
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
| import hashlib
print('you should use this execute file to decrypt "bin2"')
print('hint:md5')
s = bytearray()
f = bytearray(open('bin1.pyc', 'rb').read())
t = 'jkasnwojasd'
for i in range(0, 15):
f[i] = ((f[i] + f[i % 6]) ^ (ord(t[i % 6]) + ord(t[i % len(t)]))) % 256
s.append(f[i])
print(s)
md5_hash = hashlib.md5(bytes(s)).hexdigest()
print(md5_hash)
|
这个时候执行这个脚本，会得到一个md5a405b5d321e446459d8f9169d027bd92
之后考虑对bin2解密，用010查看bin2时会发现文件中有许多与md5类似的内容，猜测这串md5与bin2异或可以得到所需要的可执行程序
先用bin2的文件头与md5第一位xor，得到”M”，第二位则得到”Z”，那么应该就如上面所猜测一样，将md5与bin2异或后可以得到我们所需要的exe
1
2
3
4
5
6
7
8
| t = 'a405b5d321e446459d8f9169d027bd92'
with open('bin2', 'rb') as f:
data = bytearray(f.read())
result = bytearray(b ^ ord(t[i % len(t)]) for i, b in enumerate(data))
with open('output.exe', 'wb') as f:
f.write(result)
|
将得到的exe用IDA打开
加密函数为sub_1400010E0
是一个xxtea，那么main函数中的v7就是key，密文也已经有了，直接用xxtea脚本解
exp：
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
| #include <stdio.h>
#include <stdint.h>
#include<stdlib.h>
#define DELTA 0x7937B99E
#define MX ((sum ^ y) + (k[(p&3)^e] ^ z)) ^ (((16 * z) ^ (y >> 3)) + ((z >> 5) ^ (4 * y)))
void decrypt(uint32_t* v, int n, uint32_t* k) {
uint32_t y, z, sum;
unsigned p, rounds, e;
rounds = 12;
sum = rounds*DELTA;
y = v[0];
do
{
e = (sum >> 2) & 3;
for (p=n-1; p>0; p--)
{
z = v[p-1];
y = v[p] -= MX;
}
z = v[n-1];
y = v[0] -= MX;
sum -= DELTA;
} while (--rounds);
}
int main()
{
uint32_t j,m;
uint8_t v[33] = { 0xC3, 0xB5, 0x6F, 0x50, 0x45, 0x8F, 0x35, 0xB9, 0xC7, 0xE8,
0x1A, 0xC9, 0x80, 0xE2, 0x20, 0x38, 0x83, 0xBA, 0x3A, 0xD1,
0x54, 0xF5, 0x5C, 0x97, 0x6B, 0x03, 0x52, 0x43, 0x47, 0x04,
0xD2, 0x1C};
uint32_t k[4] = { 0x1234, 0x2341, 0x3412, 0x4123};
decrypt(v, 8, k);
printf(v);
system("pause");
return 0;
}
|
crackme2
IDA打开
main函数中，先是读入flag，然后使用sub_14000105C函数进行加密和验证
先看sub_14000105C函数
一个base64换表，解出来后是一个假的flag
回到main函数，看中间这个爆红，tab跳转直接看汇编
可以发现在这段代码的下面还有一段代码，但是无法被反汇编
虽然无法反汇编看，但是直接看也可以看出是对sub_14000105C函数的异或，也就是刚刚出假flag的函数
那么可以猜测是SMC，这里异或后呈现的是base64，而异或前才是真正的加密函数
那么我们可以使用ida脚本来把这个函数异或回去，其中进行异或的另一堆数据就是上面的unk_140006000
先把sub_14000105C函数undefine
然后执行如下idapython脚本
1
2
3
4
| import idc
for i in range(0x246A):
idc.patch_byte(0x14000105C + i, idc.get_db_byte(0x14000105C + i) ^ idc.get_db_byte(0x140006000 + i))
|
执行脚本后，对unk_14000105C重新创建函数，之后f5查看伪代码
此时就可以看到真正的加密函数了
一堆约束方程，使用z3规划求解
这里在比赛时因为我创建变量使用的是BitVec，跑的非常慢，挂了一个下午都没出结果
赛后看了官方wp才知道BitVec跑高维方程巨慢，使用Int一下子就可以出来了
下面脚本是赛后改用Int创建变量写的， 一下子就出结果了
exp：
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
| from z3 import *
s = Solver()
b = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31] = Ints('b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31')
s.add(b9+ 201 * b4+ 194 * b3+ 142 * b15+ 114 * b17+ 103 * b2+ 52 * (b26 + b13)+ ((b12 + b16) *64)+ 14 * (b19 + 4 * b27 + b27)+ 9 * (b7 + 23 * b11 + b21 + 3 * b25 + 4 * b21 + 4 * b23)+ 5 * (b24 + 23 * b14 + 2 * (b31 + 2 * b30) + 5 * b0 + 39 * b18 + 51 * b29)+ 24 * (b28 + 10 * b1 + 4 * (b22 + b8 + 2 * b20))+ 62 * b6+ 211 * b5+ 212 * b10 == 296473)
s.add(207 * b5+ 195 * b6+ 151 * b7+ 57 * b0+ 118 * b23+ 222 * b22+ 103 * b8+ 181 * b28+ 229 * b12+ 142 * b13+ 51 * b10+ 122 * (b20 + b15)+ 91 * (b21 + 2 * b24)+ 107 * (b11 + b27)+ 81 * (b26 + 2 * b9 + b9)+ 45 * (b30 + 2 * (b2 + b4) + b2 + b4)+ 4 * (3 * (b16 + b19 + 2 * b16 + 5 * b29) + b17 + 29 * (b3 + b25) + 25 * b18)+ 26 * b1+ 101 * b14+ 154 * b31 == 354358)
s.add(177 * b7+ 129 * b20+ 117 * b22+ 143 * b1+ 65 * b28+ 137 * b27+ 215 * b19+ 93 * b13+ 235 * b17+ 203 * b2+ 15 * (b8 + 17 * b14)+ 2* (b4+ 91 * b12+ 95 * b10+ 51 * b5+ 81 * b15+ 92 * b9+ 112 * (b3 + b23)+ 32 * (b6 + 2 * (b25 + b16))+ 6 * (b21 + 14 * b24 + 19 * b18)+ 83 * b0+ 53 * b29+ 123 * b30)+ b26+ 175 * b11+ 183 * b31 == 448573)
s.add(113 * b30+ 74 * b31+ 238 * b23+ 140 * b21+ 214 * b20+ 242 * b28+ 160 * b19+ 136 * b16+ 209 * b12+ 220 * b13+ 50 * b4+ 125 * b3+ 175 * b15+ 23 * b17+ 137 * b6+ 149 * b9+ 83 * (b29 + 2 * b14)+ 21 * (9 * b10 + b24)+ 59 * (4 * b11 + b26)+ 41 * (b25 + b5)+ 13 * (b8 + 11 * (b7 + b18) + 6 * b22 + 4 * (b1 + 2 * b2) + b1 + 2 * b2 + 17 * b0)+ 36 * b27 == 384306)
s.add(229 * b19+ 78 * b25+ b21+ b12+ 133 * b11+ 74 * b23+ 69 * b20+ 243 * b8+ 98 * b1+ 253 * b28+ 142 * b27+ 175 * b13+ 105 * b5+ 221 * b3+ 121 * b17+ 218 * (b30 + b10)+ 199 * (b4 + b14)+ 33 * (b7 + 7 * b26)+ 4 * (27 * b15 + 50 * b2 + 45 * b9 + 19 * (b31 + b22) + b24 + 16 * b16 + 52 * b29)+ 195 * b6+ 211 * b0+ 153 * b18 == 424240)
s.add(181 * b27+ 61 * b21+ 65 * b19+ 58 * b13+ 170 * b10+ 143 * b4+ 185 * b3+ 86 * b2+ 97 * b6+ 235 * (b16 + b11)+ 3* (53 * b5+ 74 * (b28 + b31)+ 13 * (b22 + 6 * b12)+ 11 * (b17 + 7 * b15)+ 15 * (b9 + 4 * b26)+ b8+ 35 * b25+ 29 * b18)+ 4 * (57 * b23 + 18 * (b0 + (2 * b20)) + b1 + 17 * b24 + 55 * b14)+ 151 * b7+ 230 * b29+ 197 * b30 == 421974)
s.add(209 * b19+ 249 * b14+ 195 * b21+ 219 * b27+ 201 * b17+ 85 * b9+ 213 * (b26 + b13)+ 119 * (b2 + 2 * b5)+ 29 * (8 * b4 + b7 + 4 * b11 + b11)+ 2* (b28+ 55 * (2 * b10 + b30)+ 3 * (b3 + 39 * b12 + 2 * (b23 + 20 * b15) + 35 * b8)+ 4 * (b0 + 31 * b22 + 28 * b31)+ 26 * b1+ 46 * ((2 * b20) + b24)+ 98 * b25)+ 53 * b16+ 171 * b18+ 123 * b29 == 442074)
s.add(162 * b30+ 74 * b0+ 28 * b11+ 243 * b22+ 123 * b1+ 73 * b28+ 166 * b16+ 94 * b4+ 113 * b2+ 193 * b6+ 122 * (b23 + 2 * b8)+ 211 * (b3 + b27)+ 21 * (b26 + 7 * b5)+ 11 * (b29 + 23 * (b24 + b17) + 2 * (b7 + 5 * b14 + 2 * (2 * b9 + b10) + 2 * b9 + b10))+ 5 * (46 * b12 + 26 * b15 + 4 * (b13 + 2 * b19) + b18 + 27 * b21 + 10 * b25)+ 36 * (b31 + 5 * b20) == 376007)
s.add(63 * b30+ 143 * b0+ 250 * b23+ 136 * b21+ 214 * b7+ 62 * b20+ 221 * b22+ 226 * b8+ 171 * b1+ 178 * b28+ 244 * b16+ (b12 *128)+ 150 * b13+ 109 * b10+ 70 * b5+ 127 * b15+ 204 * b17+ 121 * b6+ 173 * b9+ 69 * (b27 + b14 + b11)+ 74 * (b24 + 2 * b18 + b18)+ 22 * (7 * b4 + b26 + 10 * b2)+ 40 * (b25 + 4 * b19 + b19)+ 81 * b3+ 94 * b29+ 84 * b31 == 411252)
s.add(229 * b18+ 121 * b29+ 28 * b14+ 206 * b24+ 145 * b11+ 41 * b25+ 247 * b23+ 118 * b20+ 241 * b1+ 79 * b28+ 102 * b27+ 124 * b16+ 65 * b12+ 68 * b13+ 239 * b26+ 148 * b4+ 245 * b17+ 115 * b2+ 163 * b6+ 137 * b9+ 53 * (b0 + 2 * b10)+ 126 * (b7 + 2 * b3)+ 38 * (b8 + b19 + 4 * b8 + 6 * b5)+ 12 * (b21 + 16 * b22)+ 109 * b15+ 232 * b31+ 47 * b30 == 435012)
s.add(209 * b19+ 233 * b7+ 93 * b25+ 241 * b21+ 137 * b28+ 249 * b26+ 188 * b10+ 86 * b4+ 246 * b3+ 149 * b15+ 99 * b2+ 37 * b6+ 219 * b9+ 17 * (b23 + 10 * b27)+ 49 * (b0 + 3 * b31 + 4 * b1 + b1)+ 5 * (16 * b17 + 11 * (b5 + 2 * b11 + b11) + 12 * b8 + b13 + 30 * b24 + 27 * b30)+ 18 * (b16 + 2 * (b29 + b20 + 2 * b29) + b29 + b20 + 2 * b29)+ 24 * b12+ 109 * b22+ 183 * b14+ 154 * b18 == 392484)
s.add(155 * b18+ 247 * b7+ 157 * b1+ 119 * b16+ 161 * b26+ 133 * b15+ 85 * b6+ 229 * (b8 + b4)+ 123 * (2 * b13 + b22)+ 21 * (b5 + 12 * b14)+ 55 * (b12 + b0 + b9 + 2 * b0)+ 15 * (b31 + 16 * b3 + 9 * b19)+ 2* (b21+ 115 * b10+ 111 * b24+ 26 * b23+ 88 * b28+ 73 * b17+ 71 * b2+ 28 * (b20 + 2 * (b27 + 2 * b25))+ 51 * b11+ 99 * b29+ 125 * b30) == 437910)
s.add(220 * b31+ 200 * b29+ 139 * b18+ 33 * b0+ 212 * b14+ 191 * b24+ 30 * b11+ 233 * b25+ 246 * b23+ 89 * b21+ 252 * b7+ 223 * b22+ 19 * b27+ 141 * b19+ 163 * b12+ 185 * b26+ 136 * b13+ 46 * b4+ 109 * b3+ 217 * b17+ 75 * b6+ 157 * b9+ 125 * (b2 + b30)+ 104 * ((2 * b5) + b15)+ 43 * (b1 + 2 * b10 + b10)+ 32 * (b28 + b8 + 2 * b28 + 2 * (b16 + b20)) == 421905)
s.add(211 * b4+ 63 * b18+ 176 * b0+ 169 * b24+ 129 * b11+ 146 * b7+ 111 * b20+ 68 * b22+ 39 * b27+ 188 * b16+ 130 * b12+ (b13 *64)+ 91 * b5+ 208 * b15+ 145 * b17+ 247 * b9+ 93 * (b6 + b26)+ 71 * (b23 + 2 * b2)+ 103 * (b28 + 2 * b14)+ 6 * (b19 + 10 * b1 + 28 * b8 + 9 * b10 + 19 * b21 + 24 * b25 + 22 * b31)+ 81 * b3+ 70 * b29+ 23 * b30 == 356282)
s.add(94 * b22+ 101 * b21+ 152 * b7+ 200 * b8+ 226 * b28+ 211 * b16+ 121 * b4+ 74 * b2+ 166 * b9+ ((b23 + 3 * b1) *64)+ 41 * (4 * b12 + b19)+ 23 * (b17 + 11 * b5)+ 7 * (b15 + 10 * b27 + 2 * (b3 + 2 * (b13 + 4 * (b10 + b26)) + b13 + 4 * (b10 + b26)) + (b3 + 2 * (b13 + 4 * (b10 + b26)) + b13 + 4 * (b10 + b26)))+ 3 * (78 * b14 + 81 * b24 + 55 * b11 + 73 * b25 + 4 * b20 + b18 + 85 * b31 + 65 * b30)+ 62 * b6+ 88 * b0+ 110 * b29 == 423091)
s.add(133 * b6+ 175 * b18+ 181 * b14+ 199 * b24+ 123 * b11+ 242 * b25+ 75 * b23+ 69 * b21+ 153 * b7+ 33 * b20+ 100 * b22+ 229 * b8+ 177 * b28+ 134 * b13+ 179 * b10+ 129 * b5+ 14 * b3+ 247 * b4+ 228 * b15+ 92 * b2+ 86 * (b12 + (2 * b9))+ 94 * (b16 + b19)+ 37 * (b26 + 4 * b31)+ 79 * (b27 + 2 * b1)+ 72 * b0+ 93 * b17+ 152 * b29+ 214 * b30 == 391869)
s.add(211 * b4+ 213 * b9+ 197 * b7+ 159 * b27+ 117 * b19+ 119 * b12+ 98 * b26+ 218 * b5+ 106 * b17+ 69 * b2+ 43 * (b21 + b10 + 2 * b21)+ 116 * (b29 + b3 + (2 * b20))+ 5 * (b22 + 9 * b16 + 35 * b15 + 37 * b13)+ 11 * (b24 + 13 * b11 + 5 * b0 + 8 * b14)+ 6 * (29 * b1 + 25 * b28 + 38 * b6 + b18 + 13 * b25 + 10 * b31)+ 136 * b8+ 142 * b23+ 141 * b30 == 376566)
s.add(173 * b31+ 109 * b18+ 61 * b14+ 187 * b25+ 79 * b23+ 53 * b7+ 184 * b19+ 43 * b16+ 41 * b12+ 166 * b13+ 193 * b5+ 58 * b4+ 146 * b3+ (b15 *64)+ 89 * b17+ 121 * b2+ 5 * (b26 + 23 * b28)+ 7 * (29 * b9 + b10 + 4 * b8)+ 13 * (3 * b22 + b24 + 7 * b20 + 13 * b21)+ 3 * (b29 + 83 * b0 + 51 * b11 + 33 * b6 + 8 * (b30 + 4 * b1) + 18 * b27) == 300934)
s.add(78 * b25+ 131 * b0+ 185 * b24+ 250 * b7+ 90 * b20+ 129 * b22+ 255 * b1+ 206 * b28+ 239 * b27+ 150 * b3+ 253 * b17+ 104 * b6+ 58 * (b21 + 2 * b8)+ 96 * (b18 + b13)+ 117 * (b12 + 2 * b29)+ 27 * (b26 + 8 * b9 + b9)+ 19 * (b16 + 3 * b19 + 4 * b10 + b10)+ 7 * (22 * b5 + 3 * (b2 + 11 * b4) + b31 + 29 * b23 + 14 * b11)+ 109 * b15+ 102 * b14+ 100 * b30 == 401351)
s.add(233 * b30+ 71 * b0+ 209 * b11+ 82 * b23+ 58 * b20+ 53 * b27+ 113 * b16+ 206 * b13+ 39 * b5+ 163 * b15+ 222 * b2+ 191 * b9+ 123 * (b8 + b7)+ 69 * (b12 + 2 * b6 + b6)+ 9 * (b31 + 8 * b4 + 7 * (3 * b25 + b1) + 5 * b24 + 19 * b14)+ 4 * (b18 + 26 * b26 + 61 * b10 + 43 * b22 + 49 * b21 + 32 * b29)+ 10 * (7 * (b28 + (3 * b19)) + b17 + 12 * b3) == 368427)
s.add(139 * b14+ 53 * b0+ 158 * b24+ 225 * b25+ 119 * b23+ 67 * b21+ 213 * b7+ 188 * b1+ 152 * b28+ 187 * b19+ 129 * b16+ 54 * b12+ 125 * b26+ 170 * b4+ 184 * b2+ 226 * b6+ 253 * b9+ 26 * (b10 + b5)+ 97 * (b29 + 2 * b27)+ 39 * (5 * b20 + b11)+ 21 * (b17 + 8 * b22)+ 12 * (17 * b3 + b13 + 15 * b8 + 12 * b30)+ 165 * b15+ 88 * b18+ 157 * b31 == 403881)
s.add(114 * b31+ 61 * b11+ 134 * b7+ 62 * b22+ 89 * b12+ 211 * b26+ 163 * b5+ 66 * b4+ 201 * (b8 + b9)+ 47 * (5 * b24 + b6)+ 74 * (b29 + b13)+ 142 * (b21 + b1)+ 35 * (b15 + 6 * b20)+ 39 * (b18 + 6 * b14)+ 27 * (b27 + 9 * b16 + 8 * b23)+ 4 * (b19 + 63 * b30 + 2 * (b25 + 12 * (b3 + b0) + 8 * b2 + 26 * b10))+ 10 * (b28 + 4 * b17 + b17) == 382979)
s.add(122 * b27+ 225 * b19+ 52 * b16+ 253 * b12+ 197 * b26+ 187 * b13+ 181 * b10+ 183 * b5+ 47 * b15+ 229 * b17+ 88 * b6+ 127 * (b3 + (2 * b9))+ 37 * (b8 + 3 * b31)+ ((b2 + 2 * b14 + b14) *64)+ 7 * (21 * b28 + b11 + 18 * (b29 + b25 + (2 * b24)))+ 6 * (23 * b4 + b20 + 17 * b21 + 39 * b23)+ 10 * (b0 + 11 * b1 + 21 * b22)+ 149 * b30+ 165 * b7+ 121 * b18 == 435695)
s.add(165 * b15+ 223 * b29+ 249 * b0+ 199 * b25+ 135 * b21+ 133 * b20+ 254 * b22+ 111 * b8+ 189 * b1+ 221 * b27+ 115 * b19+ 186 * b12+ 79 * b5+ 217 * b4+ 122 * b2+ 38 * b9+ 109 * ((2 * b13) + b10)+ 14 * (b28 + 17 * b7 + 8 * (b23 + (2 * b24)))+ 4 * (11 * (5 * b14 + b17) + 6 * (b3 + 2 * b6) + b11 + 52 * b26 + 50 * b16)+ 229 * b18+ 86 * b31+ 234 * b30 == 453748)
s.add(181 * b27+ 94 * b22+ 125 * b25+ 226 * b20+ 155 * b8+ 95 * b19+ 212 * b26+ 91 * b13+ 194 * b10+ 98 * b4+ 166 * b2+ 120 * b6+ 59 * b9+ 32 * (b12 + b28)+ 158 * (b23 + b0)+ 101 * (b5 + b30)+ 63 * (b29 + 2 * b16)+ 67 * (b1 + 2 * b15)+ 11 * (b17 + 10 * b24 + 11 * b3)+ 39 * (b14 + 4 * (b21 + b18))+ 233 * b7+ 56 * b11+ 225 * b31 == 358321)
s.add(229 * b19+ 135 * b29+ 197 * b18+ 118 * b0+ 143 * b24+ 134 * b23+ 204 * b7+ 173 * b20+ 81 * b8+ 60 * b1+ 58 * b28+ 179 * b16+ 142 * b12+ 178 * b26+ 230 * b13+ 148 * b10+ 224 * b5+ 194 * b4+ 223 * b3+ 87 * b15+ 200 * b17+ 233 * b2+ 49 * b6+ 127 * (b27 + b14)+ 31 * (4 * b11 + b9)+ 42 * (b25 + 6 * b21)+ 109 * b22+ 75 * b31+ 165 * b30 == 456073)
s.add(41 * b29+ 253 * b31+ 163 * b18+ 193 * b14+ 155 * b24+ 113 * b11+ 131 * b23+ 55 * b21+ 21 * b7+ 53 * b20+ 13 * b28+ 201 * b27+ 237 * b12+ 223 * b13+ 95 * b4+ 194 * b15+ 62 * b17+ 119 * b2+ 171 * b6+ 135 * b9+ 69 * (b3 + 3 * b1)+ 211 * (b25 + b10)+ 4 * (43 * b8 + b22 + 40 * b26)+ 6 * (b0 + 33 * b5 + 20 * (2 * b30 + b19) + 24 * b16) == 407135)
s.add(111 * b30+ 190 * b31+ 149 * b29+ 173 * b1+ 118 * b16+ 146 * b10+ 179 * b3+ 51 * b15+ 49 * b17+ 61 * b2+ 125 * b6+ 162 * b9+ 214 * (b27 + b14)+ 14 * ((2 * b13) + b4)+ 178 * (b5 + b24)+ 11 * (4 * b12 + b19 + 17 * b22)+ 65 * (b20 + b26 + 2 * b20 + 2 * b0)+ 4 * (b8 + 38 * b18 + 4 * (b23 + b25 + 8 * b23 + 4 * (b28 + 2 * b11)) + (b23 + b25 + 8 * b23 + 4 * (b28 + 2 * b11)) + 8 * b7 + 43 * b21) == 369835)
s.add(27 * b11+ 223 * b23+ 147 * b20+ 13 * b19+ 35 * (b26 + 7 * b29)+ 57 * (b30 + (2 * b9) + 3 * b2)+ 11 * (b25 + 17 * (b12 + b0) + 10 * b24 + 3 * b13)+ 2* (53 * b16+ b27+ 38 * b18+ 43 * b22+ 115 * b10+ 61 * b6+ 111 * (b3 + b7)+ 14 * (b15 + b8 + 2 * b8 + 8 * b1)+ 109 * b21+ 100 * b5+ 63 * b28)+ 93 * b17+ 251 * b14+ 131 * b31 == 393303)
s.add(116 * b12+ 152 * b10+ 235 * b15+ 202 * b9+ 85 * (b28 + 3 * b2)+ 221 * (b24 + b7)+ 125 * ((2 * b5) + b4)+ 7 * (19 * b29 + 9 * (b3 + 2 * b27) + b21 + 33 * b31 + 32 * b30)+ 3 * (71 * b17 + 43 * b6 + 32 * (b26 + b20) + 15 * (b0 + b23 + 2 * b16) + b1 + 74 * b13 + 48 * b22)+ 10 * (b19 + 11 * b14 + 16 * b18)+ 136 * b8+ 106 * b25+ 41 * b11 == 403661)
s.add(127 * b29+ 106 * b18+ 182 * b14+ 142 * b0+ 159 * b24+ 17 * b25+ 211 * b23+ 134 * b21+ 199 * b8+ 103 * b1+ 247 * b16+ 122 * b12+ 95 * b5+ 62 * b3+ 203 * b17+ 16 * b2+ 41 * (6 * b22 + b27)+ 9 * (22 * b4 + b15 + 27 * b13 + 28 * b7)+ 10 * (b28 + b6 + (3 * b19) + 8 * b26 + 2 * (b6 + (3 * b19) + 8 * b26) + 13 * b10)+ 6 * (23 * b11 + b20)+ 213 * b9+ 179 * b31+ 43 * b30 == 418596)
s.add(149 * b30+ b25+ 133 * b6+ 207 * b5+ 182 * b20+ 234 * b8+ 199 * b28+ 168 * b19+ 58 * b3+ 108 * b15+ 142 * b9+ 156 * (b12 + b27)+ 16 * (b10 + 6 * b13)+ 126 * (b26 + 2 * b17)+ 127 * (b29 + 2 * b11 + b7)+ 49 * (b14 + 4 * b24)+ 11 * (b0 + 22 * b2)+ 5 * (b18 + b22 + 45 * b4 + 50 * b1)+ 109 * b21+ 124 * b23+ 123 * b31 == 418697)
flag = ""
print(s.check())
if s.check() == sat:
ans = s.model()
for i in range(32):
flag += chr(int("%s" % (ans[b[i]])))
print(flag)
|