babyunic-攻防世界

ctf 31 minutes read (About 4724 words)

这是第一次接触unicorn的题目，也算是第一次用z3来解决题目，花了好长时间去熟悉z3和unicorn，确实很强大

打开来有个脚本

1
LD_PRELOAD=./un.so.1 ./babyunic func

逐个调用，看一下babyunic

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

undefined8 FUN_00100eb9(int param_1,long param_2)

{
  int iVar1;
  void *__s1;
  void *pvVar2;
  
  if (param_1 == 2) {
    puts("SUCTF 2019");
    printf("input your flag:");
    __s1 = malloc(0x200);
    pvVar2 = malloc(0x200);
    __isoc99_scanf(&DAT_00101033,pvVar2);
    FUN_00100cba(pvVar2,__s1,*(undefined8 *)(param_2 + 8),__s1);
    iVar1 = memcmp(__s1,DWORD_ARRAY_00302020,0xa8);
    if (iVar1 == 0) {
      puts("congratuation!");
    }
    else {
      puts("fail!");
    }
  }
  else {
    puts("no input files");
  }
  return 0;
}

输入一个字符串经过处理后和已知字符串进行对比，相同则通过，接下来看看处理的方法

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

void FUN_00100cba(char *param_1,undefined8 param_2,char *param_3)

{
  long lVar1;
  void *__ptr;
  size_t sVar1;
  long in_FS_OFFSET;
  undefined4 local_38;
  undefined4 local_34;
  int local_30;
  undefined4 local_2c;
  undefined8 local_28;
  FILE *local_20;
  void *local_18;
  long local_10;
  
  lVar1 = *(long *)(in_FS_OFFSET + 0x28);
  local_20 = fopen(param_3,"rb");
  __ptr = malloc(0x7100);
  fread(__ptr,1,0x7100,local_20);
  local_38 = 0x101fffc0;
  local_34 = 0x101fffc0;
  local_30 = 0x101ffb00;
  local_2c = 0x101ffa00;
                    /* mips32大端序 */
  uc_open(3,0x40000004,&local_28);
  uc_mem_map(local_28,0x400000,0x200000,7);
  uc_mem_map(local_28,0x10000000,0x200000,7);
  sVar1 = strlen(param_1);
  uc_mem_write(local_28,(long)local_30,param_1,sVar1);
  uc_mem_write(local_28,0x400000,__ptr,0x7100);
  uc_reg_write(local_28,0x1f,&local_38);
  uc_reg_write(local_28,0x20,&local_34);
  uc_reg_write(local_28,7,&local_2c);
  uc_reg_write(local_28,6,&local_30);
  uc_emu_start(local_28,0x400000,0x40706c,0,0);
  uc_mem_read(local_28,0x101ffa00,param_2,200);
  uc_close(local_28);
  fclose(local_20);
  if (lVar1 != *(long *)(in_FS_OFFSET + 0x28)) {
                    /* WARNING: Subroutine does not return */
    __stack_chk_fail();
  }
  return;
}

这里用到了unicorn来模拟其它架构的处理器，查阅unicorn引用的头文件可以得到以下信息

1
2
3
4
5
6
7
8
9
10
11
12
13
local_20 = fopen(param_3,"rb");
__ptr = malloc(0x7100);
fread(__ptr,1,0x7100,local_20);
//读取输入的文件func
uc_open(3,0x40000004,&local_28);
//第一个参数3代表mips架构，第二个参数代表mips32+大端序，第三个参数是句柄
sVar1 = strlen(param_1);
uc_mem_write(local_28,(long)local_30,param_1,sVar1);
//param_1对应我们输入的字符串，放入local_30指向的地址，应该是栈
uc_mem_write(local_28,0x400000,__ptr,0x7100);
//func为可执行文件，0x400000凭经验是代码段
uc_mem_read(local_28,0x101ffa00,param_2,200);
//从栈上的某个地址读取200个字节到param_2里

最后这个函数的输出是param_2也就是最终用来比较的__s1，所以接下来需要搞清楚func函数里进行了哪些操作

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
void UndefinedFunction_00000000(byte *param_1,int *param_2)

{
  int iStack16;
  int iStack12;
  
  iStack12 = 0;
  while (param_1[iStack12] != 0) {
    iStack12 = iStack12 + 1;
  }
  iStack16 = 0;
  while (iStack16 < iStack12) {
    param_1[iStack16] = (param_1[iStack16] << 3 | param_1[iStack16] >> 5) ^ (byte)iStack16;
    iStack16 = iStack16 + 1;
  }
  *param_2 = ((((((((((((((((((((((((((((((((uint)*param_1 + (uint)param_1[1] + (uint)param_1[2]) -
                                          (uint)param_1[3]) + (uint)param_1[4]) - (uint)param_1[5])
                                       - (uint)param_1[6]) - (uint)param_1[7]) - (uint)param_1[8]) +
                                     (uint)param_1[9] + (uint)param_1[10]) - (uint)param_1[0xb]) +
                                  (uint)param_1[0xc]) - (uint)param_1[0xd]) - (uint)param_1[0xe]) +
                               (uint)param_1[0xf]) - (uint)param_1[0x10]) - (uint)param_1[0x11]) +
                             (uint)param_1[0x12] + (uint)param_1[0x13]) - (uint)param_1[0x14]) +
                           (uint)param_1[0x15] + (uint)param_1[0x16] + (uint)param_1[0x17] +
                          (uint)param_1[0x18]) - (uint)param_1[0x19]) + (uint)param_1[0x1a]) -
                       (uint)param_1[0x1b]) + (uint)param_1[0x1c] + (uint)param_1[0x1d]) -
                     (uint)param_1[0x1e]) - (uint)param_1[0x1f]) + (uint)param_1[0x20]) -
                  (uint)param_1[0x21]) + (uint)param_1[0x22] + (uint)param_1[0x23]) -
                (uint)param_1[0x24]) - (uint)param_1[0x25]) + (uint)param_1[0x26]) -
             (uint)param_1[0x27]) + (uint)param_1[0x28] + (uint)param_1[0x29];
  param_2[1] = (((((((((((((((((((((((((((((((((((uint)*param_1 - (uint)param_1[1]) +
                                               (uint)param_1[2]) - (uint)param_1[3]) -
                                             (uint)param_1[4]) + (uint)param_1[5]) -
                                           (uint)param_1[6]) - (uint)param_1[7]) - (uint)param_1[8])
                                        - (uint)param_1[9]) + (uint)param_1[10]) -
                                      (uint)param_1[0xb]) + (uint)param_1[0xc]) - (uint)param_1[0xd]
                                    ) - (uint)param_1[0xe]) + (uint)param_1[0xf]) -
                                 (uint)param_1[0x10]) - (uint)param_1[0x11]) + (uint)param_1[0x12])
                              - (uint)param_1[0x13]) + (uint)param_1[0x14] + (uint)param_1[0x15]) -
                            (uint)param_1[0x16]) - (uint)param_1[0x17]) - (uint)param_1[0x18]) +
                         (uint)param_1[0x19]) - (uint)param_1[0x1a]) + (uint)param_1[0x1b]) -
                      (uint)param_1[0x1c]) - (uint)param_1[0x1d]) + (uint)param_1[0x1e] +
                     (uint)param_1[0x1f] + (uint)param_1[0x20] + (uint)param_1[0x21] +
                     (uint)param_1[0x22] + (uint)param_1[0x23]) - (uint)param_1[0x24]) -
                  (uint)param_1[0x25]) - (uint)param_1[0x26]) - (uint)param_1[0x27]) -
               (uint)param_1[0x28]) + (uint)param_1[0x29];
  param_2[2] = ((((((((((((((((((((((((((((((uint)*param_1 - (uint)param_1[1]) + (uint)param_1[2] +
 ………………

实在是太长了，就不放全了，可以看得出来param_1是我们的输入，经过一个处理之后用一系列复杂的方程计算出了param_2

这个时候就要用z3一把梭解决问题了

首先对最终用于比较的字符进行一些处理

1
2
3
4
5
6
7
8
9
10
from z3 import *
import ctypes

e = [0xFFFFFF94, 0xFFFFFF38, 0x00000126, 0xFFFFFF28, 0xFFFFFC10, 0x00000294, 0xFFFFFC9E, 0x000006EA, 0x000000DC,
     0x00000006, 0xFFFFFF0C, 0xFFFFFDF6, 0xFFFFFA82, 0xFFFFFCD0, 0x00000182, 0x000003DE, 0x0000014E, 0x000002B2,
     0xFFFFF8D8, 0x00000174, 0xFFFFFAA6, 0xFFFFF9D4, 0x000001C2, 0xFFFFF97C, 0x0000035A, 0x00000146, 0xFFFFFF3C,
     0xFFFFFA14, 0x000001CE, 0x000007DC, 0xFFFFFD48, 0x00000098, 0x0000085E, 0xFFFFFDB0, 0xFFFFFFBC, 0x0000036E,
     0xFFFFFF4E, 0xFFFFF836, 0x000005C0, 0x000006AE, 0x00000694, 0x00000022]
en = map(lambda x: ctypes.c_int32(x).value, e)
enc = [z3.IntVal(i) for i in en]

在babyunic里是小端序存储，但是在unicorn里模拟的是32位大端序，需要进行一个转换，先是转换成大端序，然后转换成c的int32类型

1
2
3
4
5
6
7
c = [Int('c%d' % i) for i in range(42)]
flag = []
solver = Solver()

for v in c:
    solver.add(v >= 0x0)
    solver.add(v <= 0xff)

设定好符号，添加约束为ascii码值，然后添加方程的约束

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
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
solver.add(enc[0] == (((((((((((((((((((((((((((((((c[0] + c[1] + c[2]) - c[3]) + c[4]) - c[5]) - c[6]) - c[7]) - c[
    8]) + c[9] + c[10]) - c[0xb]) + c[0xc]) - c[0xd]) - c[0xe]) + c[0xf]) - c[0x10]) - c[0x11]) + c[0x12] + c[0x13]) -
                                    c[0x14]) + c[0x15] + c[0x16] + c[0x17] + c[0x18]) - c[0x19]) + c[0x1a]) - c[0x1b]) +
                               c[0x1c] + c[0x1d]) - c[0x1e]) - c[0x1f]) + c[0x20]) - c[0x21]) + c[0x22] + c[0x23]) - c[
                             0x24]) - c[0x25]) + c[0x26]) - c[0x27]) + c[0x28] + c[0x29])

solver.add(enc[1] == ((((((((((((((((((((((((((((((((((c[0] - c[1]) + c[2]) - c[3]) - c[4]) + c[5]) - c[6]) - c[7]) - c[
    8]) - c[9]) + c[10]) - c[0xb]) + c[0xc]) - c[0xd]) - c[0xe]) + c[0xf]) - c[0x10]) - c[0x11]) + c[0x12]) - c[0x13]) +
                                    c[0x14] + c[0x15]) - c[0x16]) - c[0x17]) - c[0x18]) + c[0x19]) - c[0x1a]) + c[
                                  0x1b]) - c[0x1c]) - c[0x1d]) + c[0x1e] + c[0x1f] + c[0x20] + c[0x21] + c[0x22] + c[
                               0x23]) - c[0x24]) - c[0x25]) - c[0x26]) - c[0x27]) - c[0x28]) + c[0x29])

solver.add(enc[2] == (((((((((((((((((((((((((((((c[0] - c[1]) + c[2] + c[3]) - c[4]) + c[5]) - c[6]) - c[7]) + c[8]) -
                                           c[9]) - c[10]) - c[0xb]) - c[0xc]) - c[0xd]) + c[0xe]) - c[0xf]) - c[0x10]) +
                                   c[0x11] + c[0x12] + c[0x13] + c[0x14] + c[0x15]) - c[0x16]) + c[0x17] + c[0x18] + c[
                                     0x19] + c[0x1a]) - c[0x1b]) + c[0x1c]) - c[0x1d]) + c[0x1e]) - c[0x1f]) + c[0x20] +
                           c[0x21]) - c[0x22]) - c[0x23]) + c[0x24] + c[0x25] + c[0x26]) - c[0x27]) + c[0x28]) - c[
               0x29])

solver.add(enc[3] == (((((((((((((((((((((((((((((((c[0] - c[1]) - c[2]) - c[3]) - c[4]) - c[5]) + c[6] + c[7]) - c[
    8]) - c[9]) - c[10]) - c[0xb]) + c[0xc]) - c[0xd]) + c[0xe]) - c[0xf]) + c[0x10]) - c[0x11]) + c[0x12] + c[0x13] +
                                    c[0x14]) - c[0x15]) + c[0x16] + c[0x17] + c[0x18]) - c[0x19]) - c[0x1a]) + c[
                                   0x1b]) - c[0x1c]) + c[0x1d] + c[0x1e]) - c[0x1f]) - c[0x20]) - c[0x21]) + c[0x22]) -
                        c[0x23]) + c[0x24] + c[0x25] + c[0x26]) - c[0x27]) + c[0x28] + c[0x29])

solver.add(enc[4] == (((((((((((((((((((((((((((((((((c[0] - c[1]) - c[2]) + c[3]) - c[4]) - c[5]) + c[6] + c[7] + c[
    8] + c[9]) - c[10]) + c[0xb] + c[0xc]) - c[0xd]) + c[0xe]) - c[0xf]) + c[0x10] + c[0x11]) - c[0x12]) + c[0x13]) - c[
                                            0x14]) + c[0x15]) - c[0x16]) - c[0x17]) - c[0x18]) + c[0x19]) - c[0x1a]) -
                                 c[0x1b]) - c[0x1c]) + c[0x1d] + c[0x1e] + c[0x1f]) - c[0x20]) + c[0x21]) - c[0x22]) -
                           c[0x23]) + c[0x24]) - c[0x25]) + c[0x26]) - c[0x27]) - c[0x28]) - c[0x29])

solver.add(enc[5] == ((((((((((((((((((((((((((((c[0] + c[1] + c[2] + c[3] + c[4] + c[5] + c[6] + c[7] + c[8]) - c[9]) -
                                               c[10]) - c[0xb]) - c[0xc]) - c[0xd]) - c[0xe]) + c[0xf]) - c[0x10]) + c[
                                            0x11]) - c[0x12]) + c[0x13] + c[0x14]) - c[0x15]) + c[0x16]) - c[0x17]) + c[
                                      0x18]) - c[0x19]) + c[0x1a] + c[0x1b]) - c[0x1c]) + c[0x1d]) - c[0x1e]) + c[
                                0x1f] + c[0x20] + c[0x21]) - c[0x22]) - c[0x23]) - c[0x24]) + c[0x25]) - c[0x26]) - c[
                          0x27]) + c[0x28] + c[0x29])

solver.add(enc[6] == (((((((((((((((((((((((((((c[0] - c[1]) + c[2] + c[3] + c[4]) - c[5]) + c[6] + c[7] + c[8] + c[
    9]) - c[10]) + c[0xb] + c[0xc]) - c[0xd]) + c[0xe] + c[0xf] + c[0x10] + c[0x11]) - c[0x12]) - c[0x13]) - c[0x14]) -
                                     c[0x15]) - c[0x16]) - c[0x17]) + c[0x18] + c[0x19]) - c[0x1a]) + c[0x1b] + c[
                                    0x1c] + c[0x1d]) - c[0x1e]) - c[0x1f]) - c[0x20]) - c[0x21]) - c[0x22]) - c[0x23]) +
                         c[0x24] + c[0x25]) - c[0x26]) - c[0x27]) + c[0x28]) - c[0x29])

solver.add(enc[7] == ((((((((((((((((((((((((((((((c[0] + c[1]) - c[2]) - c[3]) - c[4]) + c[5] + c[6]) - c[7]) + c[8] +
                                             c[9]) - c[10]) + c[0xb]) - c[0xc]) + c[0xd]) - c[0xe]) + c[0xf]) - c[
                                          0x10]) + c[0x11]) - c[0x12]) - c[0x13]) + c[0x14]) - c[0x15]) + c[0x16]) - c[
                                   0x17]) - c[0x18]) + c[0x19]) - c[0x1a]) + c[0x1b] + c[0x1c] + c[0x1d] + c[0x1e] + c[
                               0x1f] + c[0x20]) - c[0x21]) + c[0x22]) - c[0x23]) + c[0x24] + c[0x25] + c[0x26] + c[
                           0x27]) - c[0x28]) - c[0x29])

solver.add(enc[8] == (((((((((((((((((((((((((((((c[0] - c[1]) - c[2]) + c[3] + c[4]) - c[5]) + c[6] + c[7] + c[8] + c[
    9] + c[10]) - c[0xb]) - c[0xc]) + c[0xd]) - c[0xe]) + c[0xf] + c[0x10] + c[0x11] + c[0x12]) - c[0x13]) + c[0x14] +
                                       c[0x15]) - c[0x16]) - c[0x17]) + c[0x18] + c[0x19] + c[0x1a]) - c[0x1b]) + c[
                                      0x1c]) - c[0x1d]) - c[0x1e]) - c[0x1f]) - c[0x20]) - c[0x21]) + c[0x22]) - c[
                               0x23]) - c[0x24]) + c[0x25]) - c[0x26]) - c[0x27]) + c[0x28]) - c[0x29])

solver.add(enc[9] == (((((((((((((((((((((((((((((c[0] + c[1] + c[2]) - c[3]) + c[4] + c[5] + c[6]) - c[7]) - c[8]) - c[
    9]) - c[10]) + c[0xb] + c[0xc] + c[0xd]) - c[0xe]) + c[0xf] + c[0x10]) - c[0x11]) - c[0x12]) + c[0x13] + c[0x14]) -
                                     c[0x15]) - c[0x16]) - c[0x17]) + c[0x18]) - c[0x19]) - c[0x1a]) - c[0x1b]) + c[
                                  0x1c] + c[0x1d] + c[0x1e]) - c[0x1f]) + c[0x20] + c[0x21]) - c[0x22]) - c[0x23]) - c[
                             0x24]) - c[0x25]) + c[0x26]) - c[0x27]) + c[0x28] + c[0x29])

solver.add(enc[10] == ((((((((((((((((((((((((((((((((c[0] - c[1]) + c[2] + c[3]) - c[4]) - c[5]) + c[6] + c[7]) - c[
    8]) - c[9]) - c[10]) - c[0xb]) + c[0xc] + c[0xd] + c[0xe]) - c[0xf]) + c[0x10]) - c[0x11]) + c[0x12] + c[0x13] + c[
                                             0x14]) - c[0x15]) + c[0x16]) - c[0x17]) - c[0x18]) - c[0x19]) + c[0x1a]) -
                                  c[0x1b]) - c[0x1c]) + c[0x1d]) - c[0x1e]) + c[0x1f] + c[0x20]) - c[0x21]) - c[0x22]) +
                           c[0x23]) - c[0x24]) - c[0x25]) + c[0x26]) - c[0x27]) + c[0x28] + c[0x29])

solver.add(enc[0xb] == ((((((((((((((((((((((((((((((c[0] - c[1]) + c[2] + c[3] + c[4]) - c[5]) + c[6] + c[7]) - c[8]) +
                                                c[9] + c[10]) - c[0xb]) - c[0xc]) - c[0xd]) - c[0xe]) + c[0xf]) - c[
                                              0x10]) - c[0x11]) - c[0x12]) + c[0x13] + c[0x14]) - c[0x15]) + c[0x16]) -
                                    c[0x17]) + c[0x18] + c[0x19] + c[0x1a] + c[0x1b]) - c[0x1c]) + c[0x1d] + c[0x1e]) -
                                c[0x1f]) - c[0x20]) - c[0x21]) - c[0x22]) - c[0x23]) + c[0x24] + c[0x25]) - c[0x26]) -
                         c[0x27]) - c[0x28]) - c[0x29])

solver.add(enc[0xc] == (((((((((((((((((((((((((((((((((((((c[0] - c[1]) - c[2]) - c[3]) + c[4]) - c[5]) - c[6]) + c[
    7] + c[8]) - c[9]) + c[10]) - c[0xb]) - c[0xc]) - c[0xd]) + c[0xe]) - c[0xf]) + c[0x10]) - c[0x11]) + c[0x12]) - c[
                                               0x13]) - c[0x14]) - c[0x15]) - c[0x16]) + c[0x17]) - c[0x18]) + c[
                                         0x19]) - c[0x1a]) + c[0x1b]) - c[0x1c]) + c[0x1d]) - c[0x1e]) - c[0x1f]) + c[
                                  0x20] + c[0x21] + c[0x22]) - c[0x23]) - c[0x24]) - c[0x25]) - c[0x26]) + c[0x27]) - c[
                            0x28]) - c[0x29])

solver.add(enc[0xd] == (((((((((((((((((((((((((((((((((c[0] - c[1]) + c[2]) - c[3]) + c[4]) - c[5]) + c[6]) - c[7]) +
                                                 c[8]) - c[9]) + c[10]) - c[0xb]) + c[0xc] + c[0xd] + c[0xe] + c[0xf]) -
                                            c[0x10]) - c[0x11]) - c[0x12]) + c[0x13] + c[0x14] + c[0x15]) - c[0x16]) -
                                       c[0x17]) + c[0x18] + c[0x19]) - c[0x1a]) - c[0x1b]) + c[0x1c] + c[0x1d]) - c[
                                      0x1e]) - c[0x1f]) - c[0x20]) + c[0x21]) - c[0x22]) - c[0x23]) + c[0x24]) - c[
                               0x25]) - c[0x26]) - c[0x27]) + c[0x28]) - c[0x29])

solver.add(enc[0xe] == (((((((((((((((((((((((((c[0] + c[1] + c[2]) - c[3]) - c[4]) - c[5]) + c[6]) - c[7]) + c[8] + c[
    9] + c[10]) - c[0xb]) + c[0xc]) - c[0xd]) - c[0xe]) + c[0xf] + c[0x10] + c[0x11]) - c[0x12]) - c[0x13]) - c[0x14]) -
                                 c[0x15]) + c[0x16] + c[0x17] + c[0x18]) - c[0x19]) + c[0x1a] + c[0x1b] + c[0x1c]) - c[
                                 0x1d]) - c[0x1e]) - c[0x1f]) + c[0x20] + c[0x21] + c[0x22] + c[0x23] + c[0x24] + c[
                              0x25] + c[0x26]) - c[0x27]) - c[0x28]) - c[0x29])

solver.add(enc[0xf] == ((((((((((((((((((((((((((c[0] - c[1]) + c[2] + c[3] + c[4] + c[5]) - c[6]) + c[7]) - c[8]) - c[
    9]) - c[10]) + c[0xb] + c[0xc] + c[0xd]) - c[0xe]) - c[0xf]) - c[0x10]) + c[0x11]) - c[0x12]) - c[0x13]) - c[
                                       0x14]) - c[0x15]) + c[0x16] + c[0x17] + c[0x18] + c[0x19] + c[0x1a] + c[0x1b]) -
                                c[0x1c]) - c[0x1d]) - c[0x1e]) - c[0x1f]) + c[0x20]) - c[0x21]) + c[0x22] + c[0x23] + c[
                              0x24] + c[0x25]) - c[0x26]) + c[0x27] + c[0x28]) - c[0x29])

solver.add(enc[0x10] == ((((((((((((((((((((((((((((((c[0] - c[1]) + c[2] + c[3]) - c[4]) - c[5]) + c[6] + c[7] + c[8] +
                                                  c[9] + c[10]) - c[0xb]) + c[0xc]) - c[0xd]) + c[0xe] + c[0xf] + c[
                                                  0x10]) - c[0x11]) + c[0x12]) - c[0x13]) + c[0x14]) - c[0x15]) - c[
                                            0x16]) - c[0x17]) - c[0x18]) - c[0x19]) + c[0x1a] + c[0x1b] + c[0x1c] + c[
                                        0x1d]) - c[0x1e]) - c[0x1f]) + c[0x20]) - c[0x21]) - c[0x22]) + c[0x23]) - c[
                                 0x24]) + c[0x25]) - c[0x26]) + c[0x27]) - c[0x28]) + c[0x29])

solver.add(enc[0x11] == ((((((((((((((((((((((((((((((((c[0] + c[1] + c[2] + c[3] + c[4]) - c[5]) + c[6] + c[7] + c[
    8]) - c[9]) - c[10]) + c[0xb]) - c[0xc]) + c[0xd] + c[0xe] + c[0xf]) - c[0x10]) + c[0x11]) - c[0x12]) - c[0x13]) +
                                            c[0x14]) - c[0x15]) + c[0x16]) - c[0x17]) - c[0x18]) + c[0x19]) - c[0x1a]) +
                                     c[0x1b]) - c[0x1c]) + c[0x1d]) - c[0x1e]) - c[0x1f]) + c[0x20]) - c[0x21]) - c[
                                  0x22]) + c[0x23]) - c[0x24]) + c[0x25]) - c[0x26]) + c[0x27] + c[0x28]) - c[0x29])

solver.add(enc[0x12] == ((((((((((((((((((((((((((((((((((c[0] - c[1]) - c[2]) - c[3]) + c[4] + c[5]) - c[6]) + c[7]) -
                                                    c[8]) + c[9] + c[10]) - c[0xb]) - c[0xc]) - c[0xd]) + c[0xe]) - c[
                                                  0xf]) - c[0x10]) + c[0x11] + c[0x12] + c[0x13]) - c[0x14]) - c[
                                              0x15]) - c[0x16]) - c[0x17]) - c[0x18]) - c[0x19]) - c[0x1a]) - c[0x1b]) +
                                   c[0x1c] + c[0x1d] + c[0x1e]) - c[0x1f]) - c[0x20]) - c[0x21]) + c[0x22]) - c[0x23]) -
                             c[0x24]) - c[0x25]) - c[0x26]) - c[0x27]) - c[0x28]) + c[0x29])

solver.add(enc[0x13] == ((((((((((((((((((((((((((c[0] + c[1] + c[2] + c[3]) - c[4]) - c[5]) + c[6]) - c[7]) - c[8]) -
                                            c[9]) - c[10]) - c[0xb]) - c[0xc]) - c[0xd]) + c[0xe] + c[0xf] + c[0x10]) -
                                      c[0x11]) + c[0x12] + c[0x13] + c[0x14] + c[0x15]) - c[0x16]) + c[0x17] + c[
                                       0x18]) - c[0x19]) + c[0x1a] + c[0x1b]) - c[0x1c]) + c[0x1d] + c[0x1e] + c[0x1f] +
                               c[0x20] + c[0x21]) - c[0x22]) + c[0x23]) - c[0x24]) - c[0x25]) - c[0x26]) + c[0x27] + c[
                             0x28]) - c[0x29])

solver.add(enc[0x14] == ((((((((((((((((((((((((((((((((((((c[0] + c[1]) - c[2]) - c[3]) - c[4]) + c[5]) - c[6]) + c[
    7]) - c[8]) - c[9]) + c[10] + c[0xb]) - c[0xc]) - c[0xd]) + c[0xe]) - c[0xf]) - c[0x10]) + c[0x11]) - c[0x12]) - c[
                                               0x13]) + c[0x14] + c[0x15]) - c[0x16]) + c[0x17] + c[0x18]) - c[0x19]) -
                                      c[0x1a]) - c[0x1b]) - c[0x1c]) - c[0x1d]) - c[0x1e]) - c[0x1f]) - c[0x20]) + c[
                                   0x21]) - c[0x22]) + c[0x23] + c[0x24]) - c[0x25]) + c[0x26]) - c[0x27]) + c[0x28]) -
           c[0x29])

solver.add(enc[0x15] == (((((((((((((((((((((((((((((((((((c[0] - c[1]) - c[2]) - c[3]) + c[4] + c[5] + c[6] + c[7]) -
                                                       c[8]) - c[9]) - c[10]) - c[0xb]) - c[0xc]) - c[0xd]) - c[0xe]) -
                                                c[0xf]) - c[0x10]) + c[0x11]) - c[0x12]) - c[0x13]) + c[0x14]) - c[
                                              0x15]) + c[0x16] + c[0x17] + c[0x18]) - c[0x19]) - c[0x1a]) + c[0x1b]) -
                                     c[0x1c]) - c[0x1d]) - c[0x1e]) - c[0x1f]) - c[0x20]) - c[0x21]) - c[0x22]) - c[
                                  0x23]) - c[0x24]) + c[0x25]) - c[0x26]) - c[0x27]) - c[0x28]) + c[0x29])

solver.add(enc[0x16] == (((((((((((((((((((((((((((c[0] + c[1] + c[2] + c[3] + c[4] + c[5] + c[6] + c[7]) - c[8]) + c[
    9]) - c[10]) + c[0xb]) - c[0xc]) + c[0xd] + c[0xe] + c[0xf]) - c[0x10]) + c[0x11] + c[0x12]) - c[0x13]) - c[0x14]) +
                                        c[0x15] + c[0x16]) - c[0x17]) + c[0x18]) - c[0x19]) - c[0x1a]) + c[0x1b]) - c[
                                      0x1c]) + c[0x1d] + c[0x1e] + c[0x1f]) - c[0x20]) + c[0x21]) - c[0x22]) - c[
                                 0x23]) - c[0x24]) - c[0x25]) + c[0x26]) - c[0x27]) + c[0x28] + c[0x29])

solver.add(enc[0x17] == (((((((((((((((((((((((((((((((((((c[0] - c[1]) + c[2] + c[3]) - c[4]) - c[5]) - c[6]) - c[7]) +
                                                     c[8]) - c[9]) - c[10]) + c[0xb] + c[0xc]) - c[0xd]) - c[0xe]) + c[
                                                   0xf]) - c[0x10]) - c[0x11]) + c[0x12] + c[0x13]) - c[0x14]) - c[
                                              0x15]) + c[0x16]) - c[0x17]) + c[0x18] + c[0x19]) - c[0x1a]) + c[0x1b]) -
                                    c[0x1c]) + c[0x1d] + c[0x1e]) - c[0x1f]) - c[0x20]) - c[0x21]) - c[0x22]) - c[
                                  0x23]) - c[0x24]) - c[0x25]) + c[0x26]) - c[0x27]) - c[0x28]) - c[0x29])

solver.add(enc[0x18] == (((((((((((((((((((((((((c[0] + c[1]) - c[2]) + c[3] + c[4]) - c[5]) + c[6] + c[7]) - c[8]) + c[
    9] + c[10]) - c[0xb]) - c[0xc]) - c[0xd]) - c[0xe]) + c[0xf] + c[0x10] + c[0x11]) - c[0x12]) + c[0x13] + c[0x14] +
                                    c[0x15] + c[0x16] + c[0x17] + c[0x18] + c[0x19]) - c[0x1a]) - c[0x1b]) - c[0x1c]) +
                                c[0x1d] + c[0x1e]) - c[0x1f]) + c[0x20] + c[0x21] + c[0x22]) - c[0x23]) - c[0x24]) - c[
                               0x25]) - c[0x26]) + c[0x27] + c[0x28]) - c[0x29])

solver.add(enc[0x19] == ((((((((((((((((((((((((((((((((c[0] - c[1]) + c[2] + c[3]) - c[4]) + c[5] + c[6]) - c[7]) + c[
    8] + c[9] + c[10]) - c[0xb]) - c[0xc]) + c[0xd]) - c[0xe]) + c[0xf]) - c[0x10]) + c[0x11] + c[0x12] + c[0x13]) - c[
                                               0x14]) - c[0x15]) + c[0x16] + c[0x17]) - c[0x18]) - c[0x19]) + c[0x1a]) -
                                     c[0x1b]) + c[0x1c]) - c[0x1d]) + c[0x1e]) - c[0x1f]) - c[0x20]) + c[0x21]) - c[
                                  0x22]) - c[0x23]) - c[0x24]) - c[0x25]) + c[0x26]) - c[0x27]) + c[0x28] + c[0x29])

solver.add(enc[0x1a] == (((((((((((((((((((((((((((((c[0] + c[1] + c[2] + c[3] + c[4]) - c[5]) - c[6]) + c[7]) - c[8]) -
                                                c[9]) - c[10]) - c[0xb]) + c[0xc]) - c[0xd]) + c[0xe]) - c[0xf]) + c[
                                             0x10]) - c[0x11]) + c[0x12]) - c[0x13]) - c[0x14]) + c[0x15] + c[0x16] + c[
                                        0x17] + c[0x18] + c[0x19]) - c[0x1a]) - c[0x1b]) - c[0x1c]) - c[0x1d]) + c[
                                   0x1e] + c[0x1f]) - c[0x20]) - c[0x21]) - c[0x22]) + c[0x23] + c[0x24]) - c[0x25]) -
                         c[0x26]) + c[0x27] + c[0x28] + c[0x29])

solver.add(enc[0x1b] == (((((((((((((((((((((((((((((((c[0] - c[1]) + c[2]) - c[3]) + c[4]) - c[5]) - c[6]) - c[7]) - c[
    8]) - c[9]) - c[10]) - c[0xb]) + c[0xc] + c[0xd]) - c[0xe]) + c[0xf] + c[0x10] + c[0x11] + c[0x12] + c[0x13]) - c[
                                             0x14]) - c[0x15]) - c[0x16]) - c[0x17]) + c[0x18] + c[0x19] + c[0x1a]) - c[
                                        0x1b]) + c[0x1c] + c[0x1d] + c[0x1e]) - c[0x1f]) - c[0x20]) - c[0x21]) - c[
                                   0x22]) + c[0x23]) - c[0x24]) - c[0x25]) - c[0x26]) - c[0x27]) - c[0x28]) - c[0x29])

solver.add(enc[0x1c] == ((((((((((((((((((((((((((((((c[0] - c[1]) + c[2] + c[3] + c[4]) - c[5]) + c[6] + c[7]) - c[
    8]) - c[9]) + c[10] + c[0xb]) - c[0xc]) + c[0xd]) - c[0xe]) + c[0xf]) - c[0x10]) + c[0x11] + c[0x12] + c[0x13]) - c[
                                             0x14]) - c[0x15]) + c[0x16]) - c[0x17]) - c[0x18]) - c[0x19]) - c[0x1a]) +
                                  c[0x1b]) - c[0x1c]) - c[0x1d]) - c[0x1e]) + c[0x1f]) - c[0x20]) - c[0x21]) + c[0x22] +
                           c[0x23] + c[0x24]) - c[0x25]) - c[0x26]) + c[0x27] + c[0x28] + c[0x29])

solver.add(enc[0x1d] == ((((((((((((((((((((((((((c[0] + c[1]) - c[2]) - c[3]) - c[4]) + c[5] + c[6] + c[7]) - c[8]) +
                                            c[9]) - c[10]) - c[0xb]) + c[0xc]) - c[0xd]) + c[0xe] + c[0xf]) - c[0x10]) +
                                     c[0x11] + c[0x12]) - c[0x13]) + c[0x14] + c[0x15] + c[0x16] + c[0x17]) - c[0x18]) +
                                 c[0x19] + c[0x1a]) - c[0x1b]) + c[0x1c] + c[0x1d] + c[0x1e] + c[0x1f] + c[0x20]) - c[
                                  0x21]) - c[0x22]) + c[0x23] + c[0x24]) - c[0x25]) + c[0x26] + c[0x27]) - c[0x28]) + c[
               0x29])

solver.add(enc[0x1e] == ((((((((((((((((((((((((((((((((c[0] + c[1] + c[2] + c[3]) - c[4]) - c[5]) - c[6]) - c[7]) + c[
    8] + c[9]) - c[10]) - c[0xb]) - c[0xc]) + c[0xd]) - c[0xe]) - c[0xf]) + c[0x10]) - c[0x11]) - c[0x12]) - c[0x13]) +
                                        c[0x14]) - c[0x15]) - c[0x16]) + c[0x17] + c[0x18]) - c[0x19]) - c[0x1a]) + c[
                                      0x1b]) - c[0x1c]) - c[0x1d]) - c[0x1e]) - c[0x1f]) - c[0x20]) - c[0x21]) - c[
                               0x22]) + c[0x23] + c[0x24] + c[0x25]) - c[0x26]) + c[0x27] + c[0x28] + c[0x29])

solver.add(enc[0x1f] == ((((((((((((((((((((((((((((((c[0] + c[1]) - c[2]) + c[3] + c[4]) - c[5]) - c[6]) + c[7] + c[
    8] + c[9] + c[10] + c[0xb] + c[0xc]) - c[0xd]) - c[0xe]) - c[0xf]) + c[0x10] + c[0x11] + c[0x12] + c[0x13]) - c[
                                                0x14]) + c[0x15]) - c[0x16]) + c[0x17]) - c[0x18]) - c[0x19]) + c[
                                          0x1a] + c[0x1b]) - c[0x1c]) + c[0x1d]) - c[0x1e]) - c[0x1f]) - c[0x20]) + c[
                                    0x21]) - c[0x22]) + c[0x23]) - c[0x24]) + c[0x25]) - c[0x26]) + c[0x27]) - c[
                             0x28]) - c[0x29])

solver.add(enc[0x20] == (((((((((((((((((((((((((((c[0] - c[1]) + c[2] + c[3]) - c[4]) + c[5] + c[6] + c[7] + c[8]) - c[
    9]) + c[10] + c[0xb]) - c[0xc]) + c[0xd] + c[0xe]) - c[0xf]) + c[0x10]) - c[0x11]) + c[0x12] + c[0x13] + c[0x14]) -
                                       c[0x15]) - c[0x16]) + c[0x17]) - c[0x18]) + c[0x19] + c[0x1a] + c[0x1b]) - c[
                                      0x1c]) - c[0x1d]) - c[0x1e]) - c[0x1f]) - c[0x20]) - c[0x21]) + c[0x22] + c[
                                0x23] + c[0x24] + c[0x25]) - c[0x26]) + c[0x27]) - c[0x28]) + c[0x29])

solver.add(enc[0x21] == (((((((((((((((((((((((((((((((c[0] - c[1]) - c[2]) + c[3] + c[4] + c[5] + c[6]) - c[7]) - c[
    8]) + c[9] + c[10] + c[0xb]) - c[0xc]) - c[0xd]) + c[0xe] + c[0xf]) - c[0x10]) + c[0x11]) - c[0x12]) + c[0x13]) - c[
                                              0x14]) + c[0x15] + c[0x16] + c[0x17]) - c[0x18]) - c[0x19]) + c[0x1a] + c[
                                          0x1b]) - c[0x1c]) + c[0x1d]) - c[0x1e]) - c[0x1f]) - c[0x20]) - c[0x21]) - c[
                                   0x22]) - c[0x23]) + c[0x24]) - c[0x25]) + c[0x26]) - c[0x27]) - c[0x28]) - c[0x29])

solver.add(enc[0x22] == ((((((((((((((((((((((((((((((c[0] + c[1]) - c[2]) + c[3]) - c[4]) - c[5]) - c[6]) + c[7] + c[
    8] + c[9] + c[10] + c[0xb]) - c[0xc]) - c[0xd]) - c[0xe]) + c[0xf]) - c[0x10]) + c[0x11]) - c[0x12]) + c[0x13]) - c[
                                           0x14]) - c[0x15]) + c[0x16] + c[0x17]) - c[0x18]) - c[0x19]) + c[0x1a] + c[
                                      0x1b] + c[0x1c] + c[0x1d]) - c[0x1e]) - c[0x1f]) - c[0x20]) - c[0x21]) - c[
                                 0x22]) - c[0x23]) - c[0x24]) + c[0x25] + c[0x26] + c[0x27]) - c[0x28]) - c[0x29])

solver.add(enc[0x23] == ((((((((((((((((((((((((((c[0] - c[1]) + c[2] + c[3] + c[4]) - c[5]) - c[6]) + c[7] + c[8]) - c[
    9]) - c[10]) + c[0xb] + c[0xc] + c[0xd]) - c[0xe]) - c[0xf]) + c[0x10]) - c[0x11]) + c[0x12] + c[0x13]) - c[0x14]) -
                                    c[0x15]) - c[0x16]) + c[0x17] + c[0x18]) - c[0x19]) - c[0x1a]) + c[0x1b] + c[
                                   0x1c]) - c[0x1d]) - c[0x1e]) + c[0x1f] + c[0x20]) - c[0x21]) + c[0x22] + c[0x23] + c[
                              0x24] + c[0x25] + c[0x26] + c[0x27]) - c[0x28]) - c[0x29])

solver.add(enc[0x24] == (((((((((((((((((((((((((c[0] + c[1] + c[2]) - c[3]) - c[4]) - c[5]) - c[6]) + c[7] + c[8] + c[
    9]) - c[10]) + c[0xb] + c[0xc]) - c[0xd]) + c[0xe] + c[0xf] + c[0x10] + c[0x11] + c[0x12] + c[0x13] + c[0x14] + c[
                                            0x15]) - c[0x16]) - c[0x17]) + c[0x18]) - c[0x19]) - c[0x1a]) - c[0x1b]) -
                                 c[0x1c]) + c[0x1d] + c[0x1e] + c[0x1f] + c[0x20]) - c[0x21]) - c[0x22]) - c[0x23]) - c[
                                0x24]) + c[0x25]) - c[0x26]) + c[0x27] + c[0x28]) - c[0x29])

solver.add(enc[0x25] == ((((((((((((((((((((((((((((((((((((((c[0] - c[1]) - c[2]) + c[3]) - c[4]) + c[5]) - c[6]) - c[
    7]) - c[8]) - c[9]) + c[10]) - c[0xb]) - c[0xc]) - c[0xd]) - c[0xe]) - c[0xf]) - c[0x10]) + c[0x11] + c[0x12]) - c[
                                                 0x13]) - c[0x14]) - c[0x15]) + c[0x16]) - c[0x17]) + c[0x18]) - c[
                                           0x19]) - c[0x1a]) + c[0x1b]) - c[0x1c]) - c[0x1d]) + c[0x1e] + c[0x1f]) - c[
                                     0x20]) + c[0x21]) - c[0x22]) + c[0x23]) - c[0x24]) - c[0x25]) + c[0x26]) - c[
                              0x27]) - c[0x28]) - c[0x29])

solver.add(enc[0x26] == ((((((((((((((((((((((((((c[0] + c[1] + c[2] + c[3]) - c[4]) + c[5] + c[6] + c[7]) - c[8]) - c[
    9]) - c[10]) + c[0xb] + c[0xc] + c[0xd]) - c[0xe]) - c[0xf]) - c[0x10]) - c[0x11]) - c[0x12]) - c[0x13]) + c[0x14] +
                                     c[0x15]) - c[0x16]) + c[0x17] + c[0x18] + c[0x19] + c[0x1a] + c[0x1b]) - c[0x1c]) -
                                 c[0x1d]) + c[0x1e] + c[0x1f]) - c[0x20]) - c[0x21]) + c[0x22]) - c[0x23]) - c[0x24]) -
                          c[0x25]) + c[0x26] + c[0x27] + c[0x28]) - c[0x29])

solver.add(enc[0x27] == (((((((((((((((((((((((((c[0] - c[1]) - c[2]) - c[3]) - c[4]) + c[5]) - c[6]) - c[7]) - c[8]) +
                                         c[9]) - c[10]) + c[0xb]) - c[0xc]) + c[0xd] + c[0xe]) - c[0xf]) - c[0x10]) - c[
                                      0x11]) + c[0x12] + c[0x13] + c[0x14] + c[0x15] + c[0x16]) - c[0x17]) + c[0x18] +
                               c[0x19] + c[0x1a] + c[0x1b] + c[0x1c]) - c[0x1d]) + c[0x1e] + c[0x1f] + c[0x20] + c[
                                 0x21] + c[0x22]) - c[0x23]) - c[0x24]) + c[0x25] + c[0x26] + c[0x27]) - c[0x28]) + c[
               0x29])

solver.add(enc[0x28] == ((((((((((((((((((((((c[0] - c[1]) - c[2]) - c[3]) + c[4] + c[5] + c[6]) - c[7]) + c[8] + c[
    9]) - c[10]) + c[0xb]) - c[0xc]) - c[0xd]) - c[0xe]) + c[0xf] + c[0x10] + c[0x11] + c[0x12] + c[0x13] + c[0x14] + c[
                                       0x15] + c[0x16]) - c[0x17]) + c[0x18] + c[0x19]) - c[0x1a]) + c[0x1b] + c[
                                   0x1c]) - c[0x1d]) + c[0x1e] + c[0x1f] + c[0x20]) - c[0x21]) - c[0x22]) + c[0x23] + c[
                              0x24]) - c[0x25]) + c[0x26] + c[0x27] + c[0x28] + c[0x29])

solver.add(enc[0x29] == (((((((((((((((((((((((((((((((c[0] + c[1] + c[2] + c[3] + c[4] + c[5] + c[6]) - c[7]) - c[8]) -
                                                    c[9]) + c[10] + c[0xb]) - c[0xc]) + c[0xd]) - c[0xe]) - c[0xf]) - c[
                                                  0x10]) - c[0x11]) - c[0x12]) - c[0x13]) + c[0x14]) - c[0x15]) + c[
                                            0x16]) - c[0x17]) - c[0x18]) + c[0x19] + c[0x1a] + c[0x1b] + c[0x1c]) - c[
                                        0x1d]) - c[0x1e]) - c[0x1f]) - c[0x20]) - c[0x21]) - c[0x22]) - c[0x23]) - c[
                                 0x24]) - c[0x25]) - c[0x26]) - c[0x27]) - c[0x28]) + c[0x29])

这一部分可以直接用脚本来写，把所有的param_1替换并且注意把（uint)和*param_1特殊处理一下就好了

然后解出为唯一解

1
2
3
4
5
6
7
if solver.check() == sat:
    r = solver.model()
    for i in range(42):
        flag.append(r[c[i]].as_long() ^ i)

    flag = ''.join(map(lambda x: chr(((x >> 3) | (x << 5)) & 0xff), flag))
    print flag

直接输出flag

1
SUCTF{Un1c0rn_Engin3_Is_@_P0wer7ul_TO0ls!}

unicorn和z3实在是太好用了，之前b01lersCTF的第一道题我还愚蠢的手解方程，早知道z3一把梭就完了……

#ctf #re #攻防世界 #unicorn #z3
MRCTF-wp tar-tar-binks-攻防世界

Comments

Your browser is out-of-date!

Update your browser to view this website correctly. Update my browser now

×