filpgame

虽然比赛结束后才做出来,但还是蛮有成就感的嘿嘿

为了做出这道题,又多学了一些新知识~~

程序分析

首先,无壳32位。

然后又去百度了一下filpgame,出来了一些flipgame(翻转游戏)的内容,具体就是:一个黑白子棋盘,翻转一个棋子之后,上下左右四个棋子状态也翻转(黑变白,白变黑),最终使得棋盘所有棋子颜色统一。

带着这样一个基本概念打开IDA分析,贴一下我的分析注释:

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
int __cdecl main(int argc, const char **argv, const char **envp)
{
int v3; // eax
unsigned int ou; // ecx
unsigned int ji; // edi
char j; // si
char *v7; // eax
int jiouxing; // esi
char v9; // dl
char v10; // cl
int i; // eax
unsigned int left_right; // ebx
unsigned int up_down; // esi
__int16 *v14; // eax
char v16; // [esp+0h] [ebp-218h]
char v17; // [esp+0h] [ebp-218h]
int v18; // [esp+Ch] [ebp-20Ch]
int int_input_i_ou_; // [esp+10h] [ebp-208h]
char input[512]; // [esp+14h] [ebp-204h] BYREF

printf("Input: ", v16);
scanf("%s", (char)input);
v3 = 0;
v18 = 0;
if ( input[0] )
{
ou = int_input__ou;
ji = int_input__ji;
int_input_i_ou_ = int_input__ou;
while ( v3 < 214 ) //输入长度限制 <=214
{
j = v3;
v7 = &input[v3];
jiouxing = j & 1; // 下标奇偶判断
if ( jiouxing ) // if下标是奇数
{
v9 = *v7;
if ( (unsigned __int8)(*v7 - 48) > 9u )
{
if ( (unsigned __int8)(v9 - 65) > 0x19u )
{
ji = -1;
int_input__ji = -1;
}
else
{
ji = v9 - '7';
int_input__ji = ji;
}
}
else
{
ji = v9 - '0';
int_input__ji = ji;
}
}
else
{ // if下标是偶数
v10 = *v7;
if ( (unsigned __int8)(*v7 - 48) > 9u )
{
if ( (unsigned __int8)(v10 - 65) > 0x19u )
{
int_input__ou = -1; // >大写字母:exit
break;
}
ou = v10 - 0x37; // <=大写字母'Z'
}
else
{
ou = v10 - 0x30; // <=数字'9'
}
int_input__ou = ou;
int_input_i_ou_ = ou;
}
if ( ou > 0xF || ji > 0xF ) // 十六进制数:0~F
break;
if ( jiouxing )
{
if ( 16_int >= (int)(ou + 16 * ji) )
break;
16_int = ou + 16 * ji; // input 两个一组组成一个16进制数,奇数高位+偶数低位
for ( i = 0; i < 5; ++i )
{ // 改变状态
left_right = ou + key[i]; // key== -1,0,0,0,1
up_down = ji + key2[i]; // key2==0,0,-1,1,0
// 左 中 上 下 右
if ( left_right <= 0xF && up_down <= 0xF )
text[up_down] ^= 1 << (15 - left_right);// text[r,l]翻转:最终目的就是把每个text[i]变成0xffff
ou = int_input_i_ou_;
}
}
v3 = v18 + 1;
v18 = v3;
if ( !input[v3] )
goto LABEL_25;
}
}
else
{
LABEL_25:
v14 = text; //text有初始值
while ( *v14 == (__int16)0xFFFF ) //当text中值的每一位都变为0xFFFF
{ //也就是二进制每一位都是1
if ( (int)++v14 >= (int)&unk_BC303C )
{
printf("right, vnctf{MD5(%s)}\n", (char)input);
return 0;
}
}
}
printf("wrong\n", v17);
return 0;
}

基本逻辑就是:

  • 读入的数据都是十六进制数形式的字符(0F),其中AF是大写字母
  • text有基础值,二进制16*16的形式就是个棋盘:

    1011111011110101
    1000101110111100
    1010000011101001
    0111001100010000
    1101100100010000
    1010001110101101
    1100110010110110
    0100110111011110
    0011010001001100
    0011101111010110
    0110011100010001
    1000011010001111
    0001110001111010
    1000010000100101
    0110101100001101
    0001101101001100

  • 读入的数据,(从0开始)奇数位表示行,偶数位表示列,每两个数一组组成要改变状态的棋子的位置
  • 最后判断棋盘是否全为1,全为1即正确

分析的一些小坑

1
2
3
4
5
6
7
8
9
for ( i = 0; i < 5; ++i )
{
left_right = ou + key[i]; // key== -1,0,0,0,1
up_down = ji + key2[i]; // key2==0,0,-1,1,0
// 左 中 上 下 右
if ( left_right <= 0xF && up_down <= 0xF )
text[up_down] ^= 1 << (15 - left_right);// text[r,l]翻转:最终目的就是把每个text[i]变成0xffff
ou = int_input_i_ou_;
}

key 和 key2的值一开始不太好看出来是啥玩意,干脆动调调出来,然后再结合flipgame的概念,发现是个辅助进行各个方向棋子翻转的东西

动调的时候发现i的值是0,4,8,12,16(按理不是0~4么),有点迷惑,看汇编发现是每次i+4,>0x14时退出循环,反编译这么智能么hhh

exp

网上现成的flipgame脚本大多都是递归爆破的,16*16的棋盘规模时间复杂度差不多O(2^256)?跑到明年去。。

又看到一篇讲filp解法原理的知乎

就想到用z3列方程来解,但是一开始用z3只能出1个解,还不符合要求,又去学了下z3求多组解的方法:

就是while s.check()==sat结合s.add(Or(s.model[] != 找到的解))来实现

下面是完整的脚本:

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
from z3 import *

# map的初始数据
map = '1011111011110101100010111011110010100000111010010111001100010000110110010001000010100011101011011100110010110110010011011101111000110100010011000011101111010110011001110001000110000110100011110001110001111010100001000010010101101011000011010001101101001100'
czjz=''
x=[BitVec('x%d'%i,32) for i in range(256)]
s=Solver()
for i in range(16):
for j in range(16):
s.add(x[i*16+j]<=1)
s.add(x[i*16+j]>=0)
if i == 0 and j == 0:
s.add(int(map[i * 16 + j]) ^ (x[i*16+j]) ^ (x[(i + 1) * 16 + j]) ^ (x[i * 16 + j + 1])==1)
elif i == 15 and j == 0:
s.add(int(map[i * 16 + j]) ^ (x[i*16+j]) ^ (x[(i - 1) * 16 + j]) ^ (x[i * 16 + j + 1])==1)
elif i == 0 and j == 15:
s.add(int(map[i * 16 + j]) ^ (x[i*16+j]) ^ (x[(i + 1) * 16 + j]) ^ (x[i * 16 + j - 1])==1)
elif i == 15 and j == 15:
s.add(int(map[i * 16 + j]) ^ (x[i*16+j]) ^ (x[(i - 1) * 16 + j]) ^ (x[i * 16 + j - 1])==1)
elif i == 0:
s.add(int(map[i * 16 + j]) ^ (x[i*16+j]) ^ (x[(i + 1) * 16 + j]) ^ (x[i * 16 + j + 1]) ^ (x[i * 16 + j - 1])==1)
elif j == 0:
s.add(int(map[i * 16 + j]) ^ (x[i*16+j]) ^ (x[(i + 1) * 16 + j]) ^ (x[(i - 1) * 16 + j]) ^ (x[i * 16 + j + 1])==1)
elif i == 15:
s.add(int(map[i * 16 + j]) ^ (x[i*16+j]) ^ (x[(i - 1) * 16 + j]) ^ (x[i * 16 + j + 1]) ^ (x[i * 16 + j - 1])==1)
elif j == 15:
s.add(int(map[i * 16 + j]) ^ (x[i*16+j]) ^ (x[(i + 1) * 16 + j]) ^ (x[(i - 1) * 16 + j]) ^ (x[i * 16 + j - 1])==1)
else:
s.add(int(map[i * 16 + j]) ^ (x[i * 16 + j]) ^ (x[(i + 1) * 16 + j]) ^ (x[(i - 1) * 16 + j]) ^ (x[i * 16 + j - 1]) ^ (x[i*16 +j +1])==1)
print(s.check())
while s.check()==sat:
m=s.model()
czjz=''
for i in range(256):
czjz +=str(m[x[i]])
jiou=0
flag = [[0 for i in range(16)] for j in range(16)]
n = 0
flags=''
for i in range(16):
for j in range(16):
flag[i][j] = int(czjz[n])
n += 1
if flag[i][j] == 1:
jiou += 1
if j >= 10:
flags += chr(ord('A') + j - 10)
else:
flags += str(j)
if i >= 10:
flags += chr(ord('A') + i - 10)
else:
flags += str(i)
if jiou <=107:
print(flags)
print(jiou)
s.add(Or(x[0]!=m[x[0]],x[1]!=m[x[1]],x[2]!=m[x[2]],x[3]!=m[x[3]],x[4]!=m[x[4]],x[5]!=m[x[5]],x[6]!=m[x[6]],x[7]!=m[x[7]],x[8]!=m[x[8]],x[9]!=m[x[9]],x[10]!=m[x[10]],x[11]!=m[x[11]],x[12]!=m[x[12]],x[13]!=m[x[13]],x[14]!=m[x[14]],x[15]!=m[x[15]],x[16]!=m[x[16]],x[17]!=m[x[17]],x[18]!=m[x[18]],x[19]!=m[x[19]],x[20]!=m[x[20]],x[21]!=m[x[21]],x[22]!=m[x[22]],x[23]!=m[x[23]],x[24]!=m[x[24]],x[25]!=m[x[25]],x[26]!=m[x[26]],x[27]!=m[x[27]],x[28]!=m[x[28]],x[29]!=m[x[29]],x[30]!=m[x[30]],x[31]!=m[x[31]],x[32]!=m[x[32]],x[33]!=m[x[33]],x[34]!=m[x[34]],x[35]!=m[x[35]],x[36]!=m[x[36]],x[37]!=m[x[37]],x[38]!=m[x[38]],x[39]!=m[x[39]],x[40]!=m[x[40]],x[41]!=m[x[41]],x[42]!=m[x[42]],x[43]!=m[x[43]],x[44]!=m[x[44]],x[45]!=m[x[45]],x[46]!=m[x[46]],x[47]!=m[x[47]],x[48]!=m[x[48]],x[49]!=m[x[49]],x[50]!=m[x[50]],x[51]!=m[x[51]],x[52]!=m[x[52]],x[53]!=m[x[53]],x[54]!=m[x[54]],x[55]!=m[x[55]],x[56]!=m[x[56]],x[57]!=m[x[57]],x[58]!=m[x[58]],x[59]!=m[x[59]],x[60]!=m[x[60]],x[61]!=m[x[61]],x[62]!=m[x[62]],x[63]!=m[x[63]],x[64]!=m[x[64]],x[65]!=m[x[65]],x[66]!=m[x[66]],x[67]!=m[x[67]],x[68]!=m[x[68]],x[69]!=m[x[69]],x[70]!=m[x[70]],x[71]!=m[x[71]],x[72]!=m[x[72]],x[73]!=m[x[73]],x[74]!=m[x[74]],x[75]!=m[x[75]],x[76]!=m[x[76]],x[77]!=m[x[77]],x[78]!=m[x[78]],x[79]!=m[x[79]],x[80]!=m[x[80]],x[81]!=m[x[81]],x[82]!=m[x[82]],x[83]!=m[x[83]],x[84]!=m[x[84]],x[85]!=m[x[85]],x[86]!=m[x[86]],x[87]!=m[x[87]],x[88]!=m[x[88]],x[89]!=m[x[89]],x[90]!=m[x[90]],x[91]!=m[x[91]],x[92]!=m[x[92]],x[93]!=m[x[93]],x[94]!=m[x[94]],x[95]!=m[x[95]],x[96]!=m[x[96]],x[97]!=m[x[97]],x[98]!=m[x[98]],x[99]!=m[x[99]],x[100]!=m[x[100]],x[101]!=m[x[101]],x[102]!=m[x[102]],x[103]!=m[x[103]],x[104]!=m[x[104]],x[105]!=m[x[105]],x[106]!=m[x[106]],x[107]!=m[x[107]],x[108]!=m[x[108]],x[109]!=m[x[109]],x[110]!=m[x[110]],x[111]!=m[x[111]],x[112]!=m[x[112]],x[113]!=m[x[113]],x[114]!=m[x[114]],x[115]!=m[x[115]],x[116]!=m[x[116]],x[117]!=m[x[117]],x[118]!=m[x[118]],x[119]!=m[x[119]],x[120]!=m[x[120]],x[121]!=m[x[121]],x[122]!=m[x[122]],x[123]!=m[x[123]],x[124]!=m[x[124]],x[125]!=m[x[125]],x[126]!=m[x[126]],x[127]!=m[x[127]],x[128]!=m[x[128]],x[129]!=m[x[129]],x[130]!=m[x[130]],x[131]!=m[x[131]],x[132]!=m[x[132]],x[133]!=m[x[133]],x[134]!=m[x[134]],x[135]!=m[x[135]],x[136]!=m[x[136]],x[137]!=m[x[137]],x[138]!=m[x[138]],x[139]!=m[x[139]],x[140]!=m[x[140]],x[141]!=m[x[141]],x[142]!=m[x[142]],x[143]!=m[x[143]],x[144]!=m[x[144]],x[145]!=m[x[145]],x[146]!=m[x[146]],x[147]!=m[x[147]],x[148]!=m[x[148]],x[149]!=m[x[149]],x[150]!=m[x[150]],x[151]!=m[x[151]],x[152]!=m[x[152]],x[153]!=m[x[153]],x[154]!=m[x[154]],x[155]!=m[x[155]],x[156]!=m[x[156]],x[157]!=m[x[157]],x[158]!=m[x[158]],x[159]!=m[x[159]],x[160]!=m[x[160]],x[161]!=m[x[161]],x[162]!=m[x[162]],x[163]!=m[x[163]],x[164]!=m[x[164]],x[165]!=m[x[165]],x[166]!=m[x[166]],x[167]!=m[x[167]],x[168]!=m[x[168]],x[169]!=m[x[169]],x[170]!=m[x[170]],x[171]!=m[x[171]],x[172]!=m[x[172]],x[173]!=m[x[173]],x[174]!=m[x[174]],x[175]!=m[x[175]],x[176]!=m[x[176]],x[177]!=m[x[177]],x[178]!=m[x[178]],x[179]!=m[x[179]],x[180]!=m[x[180]],x[181]!=m[x[181]],x[182]!=m[x[182]],x[183]!=m[x[183]],x[184]!=m[x[184]],x[185]!=m[x[185]],x[186]!=m[x[186]],x[187]!=m[x[187]],x[188]!=m[x[188]],x[189]!=m[x[189]],x[190]!=m[x[190]],x[191]!=m[x[191]],x[192]!=m[x[192]],x[193]!=m[x[193]],x[194]!=m[x[194]],x[195]!=m[x[195]],x[196]!=m[x[196]],x[197]!=m[x[197]],x[198]!=m[x[198]],x[199]!=m[x[199]],x[200]!=m[x[200]],x[201]!=m[x[201]],x[202]!=m[x[202]],x[203]!=m[x[203]],x[204]!=m[x[204]],x[205]!=m[x[205]],x[206]!=m[x[206]],x[207]!=m[x[207]],x[208]!=m[x[208]],x[209]!=m[x[209]],x[210]!=m[x[210]],x[211]!=m[x[211]],x[212]!=m[x[212]],x[213]!=m[x[213]],x[214]!=m[x[214]],x[215]!=m[x[215]],x[216]!=m[x[216]],x[217]!=m[x[217]],x[218]!=m[x[218]],x[219]!=m[x[219]],x[220]!=m[x[220]],x[221]!=m[x[221]],x[222]!=m[x[222]],x[223]!=m[x[223]],x[224]!=m[x[224]],x[225]!=m[x[225]],x[226]!=m[x[226]],x[227]!=m[x[227]],x[228]!=m[x[228]],x[229]!=m[x[229]],x[230]!=m[x[230]],x[231]!=m[x[231]],x[232]!=m[x[232]],x[233]!=m[x[233]],x[234]!=m[x[234]],x[235]!=m[x[235]],x[236]!=m[x[236]],x[237]!=m[x[237]],x[238]!=m[x[238]],x[239]!=m[x[239]],x[240]!=m[x[240]],x[241]!=m[x[241]],x[242]!=m[x[242]],x[243]!=m[x[243]],x[244]!=m[x[244]],x[245]!=m[x[245]],x[246]!=m[x[246]],x[247]!=m[x[247]],x[248]!=m[x[248]],x[249]!=m[x[249]],x[250]!=m[x[250]],x[251]!=m[x[251]],x[252]!=m[x[252]],x[253]!=m[x[253]],x[254]!=m[x[254]],x[255]!=m[x[255]]))
# 遍历所有的解,这个Or的内容肯定是要自己写个脚本跑出来的
# jiou<=107是正确的解,只有一个

vnctf{md5(跑出来的结果)}

Comments