SUCTF2019-babyunic

yxtql

main函数:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
if ( a1 == 2 )
{
puts("SUCTF 2019");
printf("input your flag:", a2);
s1 = malloc(0x200uLL);
v4 = malloc(0x200uLL);
__isoc99_scanf("%50s", v4);
sub_CBA(v4, s1, *(_QWORD *)(v5 + 8));
if ( !memcmp(s1, &unk_202020, 0xA8uLL) )
puts("congratuation!");
else
puts("fail!");
}
else
{
puts("no input files");
}
return 0LL;

看上去很简单,跟进关键函数subCBA:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
stream = fopen("./func", "rb");
ptr = malloc(0x7100uLL);
fread(ptr, 1uLL, 0x7100uLL, stream);
v5 = 0x101FFFC0;
v6 = 0x101FFFC0;
v7 = 0x101FFB00;
v8 = 0x101FFA00;
uc_open(3LL, 0x40000004LL, &v9);
uc_mem_map(v9, 0x400000LL, 0x200000LL, 7LL);
uc_mem_map(v9, 0x10000000LL, 0x200000LL, 7LL);
v3 = strlen(a1);
uc_mem_write(v9, 0x101FFB00LL, a1, v3);
uc_mem_write(v9, 0x400000LL, ptr, 28928LL);
uc_reg_write(v9, 31LL, &v5);
uc_reg_write(v9, 32LL, &v6);
uc_reg_write(v9, 7LL, &v8);
uc_reg_write(v9, 6LL, &v7);
uc_emu_start(v9, 0x400000LL, 4223084LL, 0LL, 0LL);
uc_mem_read(v9, 0x101FFA00LL, a2, 200LL);
uc_close(v9);
return fclose(stream)

完全看不懂,但是通过万能的google了解到这是unicorn。分配了虚拟内存,并在其中模拟代码的执行,最后读取0x101ffa00的内存来与main函数中的输入作比较。

其中uc_open(3LL, 0x40000004LL, &v9)代表使用UC_ARCH_MIPSUC_MODE_32,特别的是0x40000004LL0x4代表了UC_MODE_32,而0x40000000代表了大端序,所以可以判断func使用的是大端序的MIPS32。

func:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
unsigned int sub_0(unsigned int param0, unsigned int param1) {
unsigned int v0 = param0, v1 = param1;
int i;

for(i = 0; *(i + v0) != 0; ++i) {
}

for(int j = 0; j < i; ++j) {
unsigned char v2 = *(j + v0);
unsigned int v3 = ((unsigned int)v2) * &loc_8;
v3 = ((unsigned int)(((unsigned char)(((unsigned int)v2) >>> 5)))) | ((int)(((unsigned char)v3)));
*(j + v0) = (unsigned char)(((int)(((unsigned char)v3))) ^ ((int)(((unsigned char)j))));
}

*v1 = ((unsigned int)(*(v0 + 1))) + ((unsigned int)(*(v0 + 2))) + ((unsigned int)(*v0)) - ((unsigned int)(*(v0 + 3))) + ((unsigned int)(*(v0 + &loc_4))) - ((unsigned int)(*(v0 + 5))) - ((unsigned int)(*(v0 + 6))) - ((unsigned int)(*(v0 + 7))) - ((unsigned int)(*(v0 + &loc_8))) + ((unsigned int)(*(v0 + 9))) + ((unsigned int)(*(v0 + 10))) - ((unsigned int)(*(v0 + 11))) + ((unsigned int)(*(v0 + &loc_C))) - ((unsigned int)(*(v0 + 13))) - ((unsigned int)(*(v0 + 14))) + ((unsigned int)(*(v0 + 15))) - ((unsigned int)(*(v0 + &loc_10))) - ((unsigned int)(*(v0 + 17))) + ((unsigned int)(*(v0 + 18))) + ((unsigned int)(*(v0 + 19))) - ((unsigned int)(*(v0 + &loc_14))) + ((unsigned int)(*(v0 + 21))) + (((unsigned int)(*(v0 + 22))) + ((unsigned int)(*(v0 + 23)))) + ((unsigned int)(*(v0 + &loc_18))) - ((unsigned int)(*(v0 + 25))) + ((unsigned int)(*(v0 + 26))) - ((unsigned int)(*(v0 + 27))) + ((unsigned int)(*(v0 + &loc_1C))) + ((unsigned int)(*(v0 + 29))) - ((unsigned int)(*(v0 + 30))) - ((unsigned int)(*(v0 + 31))) + ((unsigned int)(*(v0 + &loc_20))) - ((unsigned int)(*(v0 + 33))) + ((unsigned int)(*(v0 + 34))) + ((unsigned int)(*(v0 + 35))) - ((unsigned int)(*(v0 + &loc_24))) - ((unsigned int)(*(v0 + 37))) + ((unsigned int)(*(v0 + 38))) - ((unsigned int)(*(v0 + 39))) + ((unsigned int)(*(v0 + &loc_28))) + ((unsigned int)(*(v0 + 41)));
*(v1 + &loc_4) = ((unsigned int)(*v0)) - ((unsigned int)(*(v0 + 1))) + ((unsigned int)(*(v0 + 2))) - ((unsigned int)(*(v0 + 3))) - ((unsigned int)(*(v0 + &loc_4))) + ((unsigned int)(*(v0 + 5))) - ((unsigned int)(*(v0 + 6))) - ((unsigned int)(*(v0 + 7))) - ((unsigned int)(*(v0 + &loc_8))) - ((unsigned int)(*(v0 + 9))) + ((unsigned int)(*(v0 + 10))) - ((unsigned int)(*(v0 + 11))) + ((unsigned int)(*(v0 + &loc_C))) - ((unsigned int)(*(v0 + 13))) - ((unsigned int)(*(v0 + 14))) + ((unsigned int)(*(v0 + 15))) - ((unsigned int)(*(v0 + &loc_10))) - ((unsigned int)(*(v0 + 17))) + ((unsigned int)(*(v0 + 18))) - ((unsigned int)(*(v0 + 19))) + ((unsigned int)(*(v0 + &loc_14))) + ((unsigned int)(*(v0 + 21))) - ((unsigned int)(*(v0 + 22))) - ((unsigned int)(*(v0 + 23))) - ((unsigned int)(*(v0 + &loc_18))) + ((unsigned int)(*(v0 + 25))) - ((unsigned int)(*(v0 + 26))) + ((unsigned int)(*(v0 + 27))) - ((unsigned int)(*(v0 + &loc_1C))) - ((unsigned int)(*(v0 + 29))) + ((unsigned int)(*(v0 + 30))) + (((unsigned int)(*(v0 + 31))) + ((unsigned int)(*(v0 + &loc_20)))) + (((unsigned int)(*(v0 + 33))) + ((unsigned int)(*(v0 + 34))) + ((unsigned int)(*(v0 + 35)))) - ((unsigned int)(*(v0 + &loc_24))) - ((unsigned int)(*(v0 + 37))) - ((unsigned int)(*(v0 + 38))) - ((unsigned int)(*(v0 + 39))) - ((unsigned int)(*(v0 + &loc_28))) + ((unsigned int)(*(v0 + 41)));
*(v1 + &loc_8) = ((unsigned int)(*v0)) - ((unsigned int)(*(v0 + 1))) + ((unsigned int)(*(v0 + 2))) + ((unsigned int)(*(v0 + 3))) - ((unsigned int)(*(v0 + &loc_4))) + ((unsigned int)(*(v0 + 5))) - ((unsigned int)(*(v0 + 6))) - ((unsigned int)(*(v0 + 7))) + ((unsigned int)(*(v0 + &loc_8))) - ((unsigned int)(*(v0 + 9))) - ((unsigned int)(*(v0 + 10))) - ((unsigned int)(*(v0 + 11))) - ((unsigned int)(*(v0 + &loc_C))) - ((unsigned int)(*(v0 + 13))) + ((unsigned int)(*(v0 + 14))) - ((unsigned int)(*(v0 + 15))) - ((unsigned int)(*(v0 + &loc_10))) + ((unsigned int)(*(v0 + 17))) + (((unsigned int)(*(v0 + 18))) + ((unsigned int)(*(v0 + 19)))) + (((unsigned int)(*(v0 + &loc_14))) + ((unsigned int)(*(v0 + 21)))) - ((unsigned int)(*(v0 + 22))) + ((unsigned int)(*(v0 + 23))) + (((unsigned int)(*(v0 + &loc_18))) + ((unsigned int)(*(v0 + 25)))) + ((unsigned int)(*(v0 + 26))) - ((unsigned int)(*(v0 + 27))) + ((unsigned int)(*(v0 + &loc_1C))) - ((unsigned int)(*(v0 + 29))) + ((unsigned int)(*(v0 + 30))) - ((unsigned int)(*(v0 + 31))) + ((unsigned int)(*(v0 + &loc_20))) + ((unsigned int)(*(v0 + 33))) - ((unsigned int)(*(v0 + 34))) - ((unsigned int)(*(v0 + 35))) + ((unsigned int)(*(v0 + &loc_24))) + (((unsigned int)(*(v0 + 37))) + ((unsigned int)(*(v0 + 38)))) - ((unsigned int)(*(v0 + 39))) + ((unsigned int)(*(v0 + &loc_28))) - ((unsigned int)(*(v0 + 41)));
*(v1 + &loc_C) = ((unsigned int)(*v0)) - ((unsigned int)(*(v0 + 1))) - ((unsigned int)(*(v0 + 2))) - ((unsigned int)(*(v0 + 3))) - ((unsigned int)(*(v0 + &loc_4))) - ((unsigned int)(*(v0 + 5))) + ((unsigned int)(*(v0 + 6))) + ((unsigned int)(*(v0 + 7))) - ((unsigned int)(*(v0 + &loc_8))) - ((unsigned int)(*(v0 + 9))) - ((unsigned int)(*(v0 + 10))) - ((unsigned int)(*(v0 + 11))) + ((unsigned int)(*(v0 + &loc_C))) - ((unsigned int)(*(v0 + 13))) + ((unsigned int)(*(v0 + 14))) - ((unsigned int)(*(v0 + 15))) + ((unsigned int)(*(v0 + &loc_10))) - ((unsigned int)(*(v0 + 17))) + ((unsigned int)(*(v0 + 18))) + (((unsigned int)(*(v0 + 19))) + ((unsigned int)(*(v0 + &loc_14)))) - ((unsigned int)(*(v0 + 21))) + ((unsigned int)(*(v0 + 22))) + (((unsigned int)(*(v0 + 23))) + ((unsigned int)(*(v0 + &loc_18)))) - ((unsigned int)(*(v0 + 25))) - ((unsigned int)(*(v0 + 26))) + ((unsigned int)(*(v0 + 27))) - ((unsigned int)(*(v0 + &loc_1C))) + ((unsigned int)(*(v0 + 29))) + ((unsigned int)(*(v0 + 30))) - ((unsigned int)(*(v0 + 31))) - ((unsigned int)(*(v0 + &loc_20))) - ((unsigned int)(*(v0 + 33))) + ((unsigned int)(*(v0 + 34))) - ((unsigned int)(*(v0 + 35))) + ((unsigned int)(*(v0 + &loc_24))) + (((unsigned int)(*(v0 + 37))) + ((unsigned int)(*(v0 + 38)))) - ((unsigned int)(*(v0 + 39))) + ((unsigned int)(*(v0 + &loc_28))) + ((unsigned int)(*(v0 + 41)));
*(v1 + &loc_10) = ((unsigned int)(*v0)) - ((unsigned int)(*(v0 + 1))) - ((unsigned int)(*(v0 + 2))) + ((unsigned int)(*(v0 + 3))) - ((unsigned int)(*(v0 + &loc_4))) - ((unsigned int)(*(v0 + 5))) + ((unsigned int)(*(v0 + 6))) + (((unsigned int)(*(v0 + 7))) + ((unsigned int)(*(v0 + &loc_8)))) + ((unsigned int)(*(v0 + 9))) - ((unsigned int)(*(v0 + 10))) + ((unsigned int)(*(v0 + 11))) + ((unsigned int)(*(v0 + &loc_C))) - ((unsigned int)(*(v0 + 13))) + ((unsigned int)(*(v0 + 14))) - ((unsigned int)(*(v0 + 15))) + ((unsigned int)(*(v0 + &loc_10))) + ((unsigned int)(*(v0 + 17))) - ((unsigned int)(*(v0 + 18))) + ((unsigned int)(*(v0 + 19))) - ((unsigned int)(*(v0 + &loc_14))) + ((unsigned int)(*(v0 + 21))) - ((unsigned int)(*(v0 + 22))) - ((unsigned int)(*(v0 + 23))) - ((unsigned int)(*(v0 + &loc_18))) + ((unsigned int)(*(v0 + 25))) - ((unsigned int)(*(v0 + 26))) - ((unsigned int)(*(v0 + 27))) - ((unsigned int)(*(v0 + &loc_1C))) + ((unsigned int)(*(v0 + 29))) + (((unsigned int)(*(v0 + 30))) + ((unsigned int)(*(v0 + 31)))) - ((unsigned int)(*(v0 + &loc_20))) + ((unsigned int)(*(v0 + 33))) - ((unsigned int)(*(v0 + 34))) - ((unsigned int)(*(v0 + 35))) + ((unsigned int)(*(v0 + &loc_24))) - ((unsigned int)(*(v0 + 37))) + ((unsigned int)(*(v0 + 38))) - ((unsigned int)(*(v0 + 39))) - ((unsigned int)(*(v0 + &loc_28))) - ((unsigned int)(*(v0 + 41)));
*(v1 + &loc_14) = ((unsigned int)(*(v0 + 1))) + ((unsigned int)(*(v0 + 2))) + (((unsigned int)(*(v0 + 3))) + ((unsigned int)(*(v0 + &loc_4)))) + (((unsigned int)(*(v0 + 5))) + ((unsigned int)(*(v0 + 6))) + (((unsigned int)(*(v0 + 7))) + ((unsigned int)(*(v0 + &loc_8))))) + ((unsigned int)(*v0)) - ((unsigned int)(*(v0 + 9))) - ((unsigned int)(*(v0 + 10))) - ((unsigned int)(*(v0 + 11))) - ((unsigned int)(*(v0 + &loc_C))) - ((unsigned int)(*(v0 + 13))) - ((unsigned int)(*(v0 + 14))) + ((unsigned int)(*(v0 + 15))) - ((unsigned int)(*(v0 + &loc_10))) + ((unsigned int)(*(v0 + 17))) - ((unsigned int)(*(v0 + 18))) + ((unsigned int)(*(v0 + 19))) + ((unsigned int)(*(v0 + &loc_14))) - ((unsigned int)(*(v0 + 21))) + ((unsigned int)(*(v0 + 22))) - ((unsigned int)(*(v0 + 23))) + ((unsigned int)(*(v0 + &loc_18))) - ((unsigned int)(*(v0 + 25))) + ((unsigned int)(*(v0 + 26))) + ((unsigned int)(*(v0 + 27))) - ((unsigned int)(*(v0 + &loc_1C))) + ((unsigned int)(*(v0 + 29))) - ((unsigned int)(*(v0 + 30))) + ((unsigned int)(*(v0 + 31))) + (((unsigned int)(*(v0 + &loc_20))) + ((unsigned int)(*(v0 + 33)))) - ((unsigned int)(*(v0 + 34))) - ((unsigned int)(*(v0 + 35))) - ((unsigned int)(*(v0 + &loc_24))) + ((unsigned int)(*(v0 + 37))) - ((unsigned int)(*(v0 + 38))) - ((unsigned int)(*(v0 + 39))) + ((unsigned int)(*(v0 + &loc_28))) + ((unsigned int)(*(v0 + 41)));

省略了部分代码,可以看出是对输入进行加密后,再通过输入的42位加减计算来得到输出,最终输出来与main函数里的数组进行比较,所以就变成了一个求解42元1次方程组的问题:

贴上我的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
from z3 import *

flag=[BitVec('flag%d'%i,8)for i in range(42)]
s=[-108,-200,294,-216,-1008,660,-866,1770,220,6,-244,-522,-1406,-816,386,990,334,690,-1832,372,-1370,-1580,450,-1668,858,326,-196,-1516,462,2012,-696,152,2142,-592,-68,878,-178,-1994,1472,1710,1684,34]
solver=Solver()
solver.add(flag[1]+flag[2]+flag[0]-flag[3]+flag[4]-flag[5]-flag[6]-flag[7]-flag[8]+flag[9]+flag[10]-flag[11]+flag[12]-flag[13]-flag[14]+flag[15]-flag[16]-flag[17]+flag[18]+flag[19]-flag[20]+flag[21]+flag[22]+flag[23]+flag[24]-flag[25]+flag[26]-flag[27]+flag[28]+flag[29]-flag[30]-flag[31]+flag[32]-flag[33]+flag[34]+flag[35]-flag[36]-flag[37]+flag[38]-flag[39]+flag[40]+flag[41]==s[0])
solver.add(flag[0]-flag[1]+flag[2]-flag[3]-flag[4]+flag[5]-flag[6]-flag[7]-flag[8]-flag[9]+flag[10]-flag[11]+flag[12]-flag[13]-flag[14]+flag[15]-flag[16]-flag[17]+flag[18]-flag[19]+flag[20]+flag[21]-flag[22]-flag[23]-flag[24]+flag[25]-flag[26]+flag[27]-flag[28]-flag[29]+flag[30]+flag[31]+flag[32]+flag[33]+flag[34]+flag[35]-flag[36]-flag[37]-flag[38]-flag[39]-flag[40]+flag[41]==s[1])
solver.add(flag[0]-flag[1]+flag[2]+flag[3]-flag[4]+flag[5]-flag[6]-flag[7]+flag[8]-flag[9]-flag[10]-flag[11]-flag[12]-flag[13]+flag[14]-flag[15]-flag[16]+flag[17]+flag[18]+flag[19]+flag[20]+flag[21]-flag[22]+flag[23]+flag[24]+flag[25]+flag[26]-flag[27]+flag[28]-flag[29]+flag[30]-flag[31]+flag[32]+flag[33]-flag[34]-flag[35]+flag[36]+flag[37]+flag[38]-flag[39]+flag[40]-flag[41]==s[2])
solver.add(flag[0]-flag[1]-flag[2]-flag[3]-flag[4]-flag[5]+flag[6]+flag[7]-flag[8]-flag[9]-flag[10]-flag[11]+flag[12]-flag[13]+flag[14]-flag[15]+flag[16]-flag[17]+flag[18]+flag[19]+flag[20]-flag[21]+flag[22]+flag[23]+flag[24]-flag[25]-flag[26]+flag[27]-flag[28]+flag[29]+flag[30]-flag[31]-flag[32]-flag[33]+flag[34]-flag[35]+flag[36]+flag[37]+flag[38]-flag[39]+flag[40]+flag[41]==s[3])
solver.add(flag[0]-flag[1]-flag[2]+flag[3]-flag[4]-flag[5]+flag[6]+flag[7]+flag[8]+flag[9]-flag[10]+flag[11]+flag[12]-flag[13]+flag[14]-flag[15]+flag[16]+flag[17]-flag[18]+flag[19]-flag[20]+flag[21]-flag[22]-flag[23]-flag[24]+flag[25]-flag[26]-flag[27]-flag[28]+flag[29]+flag[30]+flag[31]-flag[32]+flag[33]-flag[34]-flag[35]+flag[36]-flag[37]+flag[38]-flag[39]-flag[40]-flag[41]==s[4])
solver.add(flag[1]+flag[2]+flag[3]+flag[4]+flag[5]+flag[6]+flag[7]+flag[8]+flag[0]-flag[9]-flag[10]-flag[11]-flag[12]-flag[13]-flag[14]+flag[15]-flag[16]+flag[17]-flag[18]+flag[19]+flag[20]-flag[21]+flag[22]-flag[23]+flag[24]-flag[25]+flag[26]+flag[27]-flag[28]+flag[29]-flag[30]+flag[31]+flag[32]+flag[33]-flag[34]-flag[35]-flag[36]+flag[37]-flag[38]-flag[39]+flag[40]+flag[41]==s[5])
solver.add(flag[0]-flag[1]+flag[2]+flag[3]+flag[4]-flag[5]+flag[6]+flag[7]+flag[8]+flag[9]-flag[10]+flag[11]+flag[12]-flag[13]+flag[14]+flag[15]+flag[16]+flag[17]-flag[18]-flag[19]-flag[20]-flag[21]-flag[22]-flag[23]+flag[24]+flag[25]-flag[26]+flag[27]+flag[28]+flag[29]-flag[30]-flag[31]-flag[32]-flag[33]-flag[34]-flag[35]+flag[36]+flag[37]-flag[38]-flag[39]+flag[40]-flag[41]==s[6])
solver.add(flag[1]+flag[0]-flag[2]-flag[3]-flag[4]+flag[5]+flag[6]-flag[7]+flag[8]+flag[9]-flag[10]+flag[11]-flag[12]+flag[13]-flag[14]+flag[15]-flag[16]+flag[17]-flag[18]-flag[19]+flag[20]-flag[21]+flag[22]-flag[23]-flag[24]+flag[25]-flag[26]+flag[27]+flag[28]+flag[29]+flag[30]+flag[31]+flag[32]-flag[33]+flag[34]-flag[35]+flag[36]+flag[37]+flag[38]+flag[39]-flag[40]-flag[41]==s[7])
solver.add(flag[0]-flag[1]-flag[2]+flag[3]+flag[4]-flag[5]+flag[6]+flag[7]+flag[8]+flag[9]+flag[10]-flag[11]-flag[12]+flag[13]-flag[14]+flag[15]+flag[16]+flag[17]+flag[18]-flag[19]+flag[20]+flag[21]-flag[22]-flag[23]+flag[24]+flag[25]+flag[26]-flag[27]+flag[28]-flag[29]-flag[30]-flag[31]-flag[32]-flag[33]+flag[34]-flag[35]-flag[36]+flag[37]-flag[38]-flag[39]+flag[40]-flag[41]==s[8])
solver.add(flag[1]+flag[2]+flag[0]-flag[3]+flag[4]+flag[5]+flag[6]-flag[7]-flag[8]-flag[9]-flag[10]+flag[11]+flag[12]+flag[13]-flag[14]+flag[15]+flag[16]-flag[17]-flag[18]+flag[19]+flag[20]-flag[21]-flag[22]-flag[23]+flag[24]-flag[25]-flag[26]-flag[27]+flag[28]+flag[29]+flag[30]-flag[31]+flag[32]+flag[33]-flag[34]-flag[35]-flag[36]-flag[37]+flag[38]-flag[39]+flag[40]+flag[41]==s[9])
solver.add(flag[0]-flag[1]+flag[2]+flag[3]-flag[4]-flag[5]+flag[6]+flag[7]-flag[8]-flag[9]-flag[10]-flag[11]+flag[12]+flag[13]+flag[14]-flag[15]+flag[16]-flag[17]+flag[18]+flag[19]+flag[20]-flag[21]+flag[22]-flag[23]-flag[24]-flag[25]+flag[26]-flag[27]-flag[28]+flag[29]-flag[30]+flag[31]+flag[32]-flag[33]-flag[34]+flag[35]-flag[36]-flag[37]+flag[38]-flag[39]+flag[40]+flag[41]==s[10])
solver.add(flag[0]-flag[1]+flag[2]+flag[3]+flag[4]-flag[5]+flag[6]+flag[7]-flag[8]+flag[9]+flag[10]-flag[11]-flag[12]-flag[13]-flag[14]+flag[15]-flag[16]-flag[17]-flag[18]+flag[19]+flag[20]-flag[21]+flag[22]-flag[23]+flag[24]+flag[25]+flag[26]+flag[27]-flag[28]+flag[29]+flag[30]-flag[31]-flag[32]-flag[33]-flag[34]-flag[35]+flag[36]+flag[37]-flag[38]-flag[39]-flag[40]-flag[41]==s[11])
solver.add(flag[0]-flag[1]-flag[2]-flag[3]+flag[4]-flag[5]-flag[6]+flag[7]+flag[8]-flag[9]+flag[10]-flag[11]-flag[12]-flag[13]+flag[14]-flag[15]+flag[16]-flag[17]+flag[18]-flag[19]-flag[20]-flag[21]-flag[22]+flag[23]-flag[24]+flag[25]-flag[26]+flag[27]-flag[28]+flag[29]-flag[30]-flag[31]+flag[32]+flag[33]+flag[34]-flag[35]-flag[36]-flag[37]-flag[38]+flag[39]-flag[40]-flag[41]==s[12])
solver.add(flag[0]-flag[1]+flag[2]-flag[3]+flag[4]-flag[5]+flag[6]-flag[7]+flag[8]-flag[9]+flag[10]-flag[11]+flag[12]+flag[13]+flag[14]+flag[15]-flag[16]-flag[17]-flag[18]+flag[19]+flag[20]+flag[21]-flag[22]-flag[23]+flag[24]+flag[25]-flag[26]-flag[27]+flag[28]+flag[29]-flag[30]-flag[31]-flag[32]+flag[33]-flag[34]-flag[35]+flag[36]-flag[37]-flag[38]-flag[39]+flag[40]-flag[41]==s[13])
solver.add(flag[1]+flag[2]+flag[0]-flag[3]-flag[4]-flag[5]+flag[6]-flag[7]+flag[8]+flag[9]+flag[10]-flag[11]+flag[12]-flag[13]-flag[14]+flag[15]+flag[16]+flag[17]-flag[18]-flag[19]-flag[20]-flag[21]+flag[22]+flag[23]+flag[24]-flag[25]+flag[26]+flag[27]+flag[28]-flag[29]-flag[30]-flag[31]+flag[32]+flag[33]+flag[34]+flag[35]+flag[36]+flag[37]+flag[38]-flag[39]-flag[40]-flag[41]==s[14])
solver.add(flag[0]-flag[1]+flag[2]+flag[3]+flag[4]+flag[5]-flag[6]+flag[7]-flag[8]-flag[9]-flag[10]+flag[11]+flag[12]+flag[13]-flag[14]-flag[15]-flag[16]+flag[17]-flag[18]-flag[19]-flag[20]-flag[21]+flag[22]+flag[23]+flag[24]+flag[25]+flag[26]+flag[27]-flag[28]-flag[29]-flag[30]-flag[31]+flag[32]-flag[33]+flag[34]+flag[35]+flag[36]+flag[37]-flag[38]+flag[39]+flag[40]-flag[41]==s[15])
solver.add(flag[0]-flag[1]+flag[2]+flag[3]-flag[4]-flag[5]+flag[6]+flag[7]+flag[8]+flag[9]+flag[10]-flag[11]+flag[12]-flag[13]+flag[14]+flag[15]+flag[16]-flag[17]+flag[18]-flag[19]+flag[20]-flag[21]-flag[22]-flag[23]-flag[24]-flag[25]+flag[26]+flag[27]+flag[28]+flag[29]-flag[30]-flag[31]+flag[32]-flag[33]-flag[34]+flag[35]-flag[36]+flag[37]-flag[38]+flag[39]-flag[40]+flag[41]==s[16])
solver.add(flag[1]+flag[2]+flag[3]+flag[4]+flag[0]-flag[5]+flag[6]+flag[7]+flag[8]-flag[9]-flag[10]+flag[11]-flag[12]+flag[13]+flag[14]+flag[15]-flag[16]+flag[17]-flag[18]-flag[19]+flag[20]-flag[21]+flag[22]-flag[23]-flag[24]+flag[25]-flag[26]+flag[27]-flag[28]+flag[29]-flag[30]-flag[31]+flag[32]-flag[33]-flag[34]+flag[35]-flag[36]+flag[37]-flag[38]+flag[39]+flag[40]-flag[41]==s[17])
solver.add(flag[0]-flag[1]-flag[2]-flag[3]+flag[4]+flag[5]-flag[6]+flag[7]-flag[8]+flag[9]+flag[10]-flag[11]-flag[12]-flag[13]+flag[14]-flag[15]-flag[16]+flag[17]+flag[18]+flag[19]-flag[20]-flag[21]-flag[22]-flag[23]-flag[24]-flag[25]-flag[26]-flag[27]+flag[28]+flag[29]+flag[30]-flag[31]-flag[32]-flag[33]+flag[34]-flag[35]-flag[36]-flag[37]-flag[38]-flag[39]-flag[40]+flag[41]==s[18])
solver.add(flag[1]+flag[2]+flag[3]+flag[0]-flag[4]-flag[5]+flag[6]-flag[7]-flag[8]-flag[9]-flag[10]-flag[11]-flag[12]-flag[13]+flag[14]+flag[15]+flag[16]-flag[17]+flag[18]+flag[19]+flag[20]+flag[21]-flag[22]+flag[23]+flag[24]-flag[25]+flag[26]+flag[27]-flag[28]+flag[29]+flag[30]+flag[31]+flag[32]+flag[33]-flag[34]+flag[35]-flag[36]-flag[37]-flag[38]+flag[39]+flag[40]-flag[41]==s[19])
solver.add(flag[1]+flag[0]-flag[2]-flag[3]-flag[4]+flag[5]-flag[6]+flag[7]-flag[8]-flag[9]+flag[10]+flag[11]-flag[12]-flag[13]+flag[14]-flag[15]-flag[16]+flag[17]-flag[18]-flag[19]+flag[20]+flag[21]-flag[22]+flag[23]+flag[24]-flag[25]-flag[26]-flag[27]-flag[28]-flag[29]-flag[30]-flag[31]-flag[32]+flag[33]-flag[34]+flag[35]+flag[36]-flag[37]+flag[38]-flag[39]+flag[40]-flag[41]==s[20])
solver.add(flag[0]-flag[1]-flag[2]-flag[3]+flag[4]+flag[5]+flag[6]+flag[7]-flag[8]-flag[9]-flag[10]-flag[11]-flag[12]-flag[13]-flag[14]-flag[15]-flag[16]+flag[17]-flag[18]-flag[19]+flag[20]-flag[21]+flag[22]+flag[23]+flag[24]-flag[25]-flag[26]+flag[27]-flag[28]-flag[29]-flag[30]-flag[31]-flag[32]-flag[33]-flag[34]-flag[35]-flag[36]+flag[37]-flag[38]-flag[39]-flag[40]+flag[41]==s[21])
solver.add(flag[1]+flag[2]+flag[3]+flag[4]+flag[5]+flag[6]+flag[7]+flag[0]-flag[8]+flag[9]-flag[10]+flag[11]-flag[12]+flag[13]+flag[14]+flag[15]-flag[16]+flag[17]+flag[18]-flag[19]-flag[20]+flag[21]+flag[22]-flag[23]+flag[24]-flag[25]-flag[26]+flag[27]-flag[28]+flag[29]+flag[30]+flag[31]-flag[32]+flag[33]-flag[34]-flag[35]-flag[36]-flag[37]+flag[38]-flag[39]+flag[40]+flag[41]==s[22])
solver.add(flag[0]-flag[1]+flag[2]+flag[3]-flag[4]-flag[5]-flag[6]-flag[7]+flag[8]-flag[9]-flag[10]+flag[11]+flag[12]-flag[13]-flag[14]+flag[15]-flag[16]-flag[17]+flag[18]+flag[19]-flag[20]-flag[21]+flag[22]-flag[23]+flag[24]+flag[25]-flag[26]+flag[27]-flag[28]+flag[29]+flag[30]-flag[31]-flag[32]-flag[33]-flag[34]-flag[35]-flag[36]-flag[37]+flag[38]-flag[39]-flag[40]-flag[41]==s[23])
solver.add(flag[1]+flag[0]-flag[2]+flag[3]+flag[4]-flag[5]+flag[6]+flag[7]-flag[8]+flag[9]+flag[10]-flag[11]-flag[12]-flag[13]-flag[14]+flag[15]+flag[16]+flag[17]-flag[18]+flag[19]+flag[20]+flag[21]+flag[22]+flag[23]+flag[24]+flag[25]-flag[26]-flag[27]-flag[28]+flag[29]+flag[30]-flag[31]+flag[32]+flag[33]+flag[34]-flag[35]-flag[36]-flag[37]-flag[38]+flag[39]+flag[40]-flag[41]==s[24])
solver.add(flag[0]-flag[1]+flag[2]+flag[3]-flag[4]+flag[5]+flag[6]-flag[7]+flag[8]+flag[9]+flag[10]-flag[11]-flag[12]+flag[13]-flag[14]+flag[15]-flag[16]+flag[17]+flag[18]+flag[19]-flag[20]-flag[21]+flag[22]+flag[23]-flag[24]-flag[25]+flag[26]-flag[27]+flag[28]-flag[29]+flag[30]-flag[31]-flag[32]+flag[33]-flag[34]-flag[35]-flag[36]-flag[37]+flag[38]-flag[39]+flag[40]+flag[41]==s[25])
solver.add(flag[1]+flag[2]+flag[3]+flag[4]+flag[0]-flag[5]-flag[6]+flag[7]-flag[8]-flag[9]-flag[10]-flag[11]+flag[12]-flag[13]+flag[14]-flag[15]+flag[16]-flag[17]+flag[18]-flag[19]-flag[20]+flag[21]+flag[22]+flag[23]+flag[24]+flag[25]-flag[26]-flag[27]-flag[28]-flag[29]+flag[30]+flag[31]-flag[32]-flag[33]-flag[34]+flag[35]+flag[36]-flag[37]-flag[38]+flag[39]+flag[40]+flag[41]==s[26])
solver.add(flag[0]-flag[1]+flag[2]-flag[3]+flag[4]-flag[5]-flag[6]-flag[7]-flag[8]-flag[9]-flag[10]-flag[11]+flag[12]+flag[13]-flag[14]+flag[15]+flag[16]+flag[17]+flag[18]+flag[19]-flag[20]-flag[21]-flag[22]-flag[23]+flag[24]+flag[25]+flag[26]-flag[27]+flag[28]+flag[29]+flag[30]-flag[31]-flag[32]-flag[33]-flag[34]+flag[35]-flag[36]-flag[37]-flag[38]-flag[39]-flag[40]-flag[41]==s[27])
solver.add(flag[0]-flag[1]+flag[2]+flag[3]+flag[4]-flag[5]+flag[6]+flag[7]-flag[8]-flag[9]+flag[10]+flag[11]-flag[12]+flag[13]-flag[14]+flag[15]-flag[16]+flag[17]+flag[18]+flag[19]-flag[20]-flag[21]+flag[22]-flag[23]-flag[24]-flag[25]-flag[26]+flag[27]-flag[28]-flag[29]-flag[30]+flag[31]-flag[32]-flag[33]+flag[34]+flag[35]+flag[36]-flag[37]-flag[38]+flag[39]+flag[40]+flag[41]==s[28])
solver.add(flag[1]+flag[0]-flag[2]-flag[3]-flag[4]+flag[5]+flag[6]+flag[7]-flag[8]+flag[9]-flag[10]-flag[11]+flag[12]-flag[13]+flag[14]+flag[15]-flag[16]+flag[17]+flag[18]-flag[19]+flag[20]+flag[21]+flag[22]+flag[23]-flag[24]+flag[25]+flag[26]-flag[27]+flag[28]+flag[29]+flag[30]+flag[31]+flag[32]-flag[33]-flag[34]+flag[35]+flag[36]-flag[37]+flag[38]+flag[39]-flag[40]+flag[41]==s[29])
solver.add(flag[1]+flag[2]+flag[3]+flag[0]-flag[4]-flag[5]-flag[6]-flag[7]+flag[8]+flag[9]-flag[10]-flag[11]-flag[12]+flag[13]-flag[14]-flag[15]+flag[16]-flag[17]-flag[18]-flag[19]+flag[20]-flag[21]-flag[22]+flag[23]+flag[24]-flag[25]-flag[26]+flag[27]-flag[28]-flag[29]-flag[30]-flag[31]-flag[32]-flag[33]-flag[34]+flag[35]+flag[36]+flag[37]-flag[38]+flag[39]+flag[40]+flag[41]==s[30])
solver.add(flag[1]+flag[0]-flag[2]+flag[3]+flag[4]-flag[5]-flag[6]+flag[7]+flag[8]+flag[9]+flag[10]+flag[11]+flag[12]-flag[13]-flag[14]-flag[15]+flag[16]+flag[17]+flag[18]+flag[19]-flag[20]+flag[21]-flag[22]+flag[23]-flag[24]-flag[25]+flag[26]+flag[27]-flag[28]+flag[29]-flag[30]-flag[31]-flag[32]+flag[33]-flag[34]+flag[35]-flag[36]+flag[37]-flag[38]+flag[39]-flag[40]-flag[41]==s[31])
solver.add(flag[0]-flag[1]+flag[2]+flag[3]-flag[4]+flag[5]+flag[6]+flag[7]+flag[8]-flag[9]+flag[10]+flag[11]-flag[12]+flag[13]+flag[14]-flag[15]+flag[16]-flag[17]+flag[18]+flag[19]+flag[20]-flag[21]-flag[22]+flag[23]-flag[24]+flag[25]+flag[26]+flag[27]-flag[28]-flag[29]-flag[30]-flag[31]-flag[32]-flag[33]+flag[34]+flag[35]+flag[36]+flag[37]-flag[38]+flag[39]-flag[40]+flag[41]==s[32])
solver.add(flag[0]-flag[1]-flag[2]+flag[3]+flag[4]+flag[5]+flag[6]-flag[7]-flag[8]+flag[9]+flag[10]+flag[11]-flag[12]-flag[13]+flag[14]+flag[15]-flag[16]+flag[17]-flag[18]+flag[19]-flag[20]+flag[21]+flag[22]+flag[23]-flag[24]-flag[25]+flag[26]+flag[27]-flag[28]+flag[29]-flag[30]-flag[31]-flag[32]-flag[33]-flag[34]-flag[35]+flag[36]-flag[37]+flag[38]-flag[39]-flag[40]-flag[41]==s[33])
solver.add(flag[1]+flag[0]-flag[2]+flag[3]-flag[4]-flag[5]-flag[6]+flag[7]+flag[8]+flag[9]+flag[10]+flag[11]-flag[12]-flag[13]-flag[14]+flag[15]-flag[16]+flag[17]-flag[18]+flag[19]-flag[20]-flag[21]+flag[22]+flag[23]-flag[24]-flag[25]+flag[26]+flag[27]+flag[28]+flag[29]-flag[30]-flag[31]-flag[32]-flag[33]-flag[34]-flag[35]-flag[36]+flag[37]+flag[38]+flag[39]-flag[40]-flag[41]==s[34])
solver.add(flag[0]-flag[1]+flag[2]+flag[3]+flag[4]-flag[5]-flag[6]+flag[7]+flag[8]-flag[9]-flag[10]+flag[11]+flag[12]+flag[13]-flag[14]-flag[15]+flag[16]-flag[17]+flag[18]+flag[19]-flag[20]-flag[21]-flag[22]+flag[23]+flag[24]-flag[25]-flag[26]+flag[27]+flag[28]-flag[29]-flag[30]+flag[31]+flag[32]-flag[33]+flag[34]+flag[35]+flag[36]+flag[37]+flag[38]+flag[39]-flag[40]-flag[41]==s[35])
solver.add(flag[1]+flag[2]+flag[0]-flag[3]-flag[4]-flag[5]-flag[6]+flag[7]+flag[8]+flag[9]-flag[10]+flag[11]+flag[12]-flag[13]+flag[14]+flag[15]+flag[16]+flag[17]+flag[18]+flag[19]+flag[20]+flag[21]-flag[22]-flag[23]+flag[24]-flag[25]-flag[26]-flag[27]-flag[28]+flag[29]+flag[30]+flag[31]+flag[32]-flag[33]-flag[34]-flag[35]-flag[36]+flag[37]-flag[38]+flag[39]+flag[40]-flag[41]==s[36])
solver.add(flag[0]-flag[1]-flag[2]+flag[3]-flag[4]+flag[5]-flag[6]-flag[7]-flag[8]-flag[9]+flag[10]-flag[11]-flag[12]-flag[13]-flag[14]-flag[15]-flag[16]+flag[17]+flag[18]-flag[19]-flag[20]-flag[21]+flag[22]-flag[23]+flag[24]-flag[25]-flag[26]+flag[27]-flag[28]-flag[29]+flag[30]+flag[31]-flag[32]+flag[33]-flag[34]+flag[35]-flag[36]-flag[37]+flag[38]-flag[39]-flag[40]-flag[41]==s[37])
solver.add(flag[1]+flag[2]+flag[3]+flag[0]-flag[4]+flag[5]+flag[6]+flag[7]-flag[8]-flag[9]-flag[10]+flag[11]+flag[12]+flag[13]-flag[14]-flag[15]-flag[16]-flag[17]-flag[18]-flag[19]+flag[20]+flag[21]-flag[22]+flag[23]+flag[24]+flag[25]+flag[26]+flag[27]-flag[28]-flag[29]+flag[30]+flag[31]-flag[32]-flag[33]+flag[34]-flag[35]-flag[36]-flag[37]+flag[38]+flag[39]+flag[40]-flag[41]==s[38])
solver.add(flag[0]-flag[1]-flag[2]-flag[3]-flag[4]+flag[5]-flag[6]-flag[7]-flag[8]+flag[9]-flag[10]+flag[11]-flag[12]+flag[13]+flag[14]-flag[15]-flag[16]-flag[17]+flag[18]+flag[19]+flag[20]+flag[21]+flag[22]-flag[23]+flag[24]+flag[25]+flag[26]+flag[27]+flag[28]-flag[29]+flag[30]+flag[31]+flag[32]+flag[33]+flag[34]-flag[35]-flag[36]+flag[37]+flag[38]+flag[39]-flag[40]+flag[41]==s[39])
solver.add(flag[0]-flag[1]-flag[2]-flag[3]+flag[4]+flag[5]+flag[6]-flag[7]+flag[8]+flag[9]-flag[10]+flag[11]-flag[12]-flag[13]-flag[14]+flag[15]+flag[16]+flag[17]+flag[18]+flag[19]+flag[20]+flag[21]+flag[22]-flag[23]+flag[24]+flag[25]-flag[26]+flag[27]+flag[28]-flag[29]+flag[30]+flag[31]+flag[32]-flag[33]-flag[34]+flag[35]+flag[36]-flag[37]+flag[38]+flag[39]+flag[40]+flag[41]==s[40])
solver.add(flag[1]+flag[2]+flag[3]+flag[4]+flag[5]+flag[6]+flag[0]-flag[7]-flag[8]-flag[9]+flag[10]+flag[11]-flag[12]+flag[13]-flag[14]-flag[15]-flag[16]-flag[17]-flag[18]-flag[19]+flag[20]-flag[21]+flag[22]-flag[23]-flag[24]+flag[25]+flag[26]+flag[27]+flag[28]-flag[29]-flag[30]-flag[31]-flag[32]-flag[33]-flag[34]-flag[35]-flag[36]-flag[37]-flag[38]-flag[39]-flag[40]+flag[41]==s[41])
if solver.check()==sat:
print solver.model()

不过解了半天也没解出来2333,最后是密码学大佬yx解的方程,

(换成Int就解出来了)

最后再逆运算一下得到flag

1
2
3
4
5
6
7
s2=[154, 171, 24, 161, 54, 222, 172, 116, 129, 18, 139, 152, 127, 247, 36, 124, 43, 90, 97, 138, 238, 95, 141, 237, 26, 227, 152, 154, 167, 54, 141, 166, 139, 66, 216, 129, 94, 164, 69, 188, 33, 194]
for i in range(len(s2)):
s2[i]^=i
s2[i]=(s2[i]>>3)|(s2[i]<<5)
s2[i]=s2[i]&0xff
print ''.join([chr(i) for i in s2])
#SUCTF{Un1c0rn_Engin3_Is_@_P0wer7ul_TO0ls!}
文章目录
|