filpgame

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

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

程序分析

首先，无壳32位。

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

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

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;
}

基本逻辑就是：

读入的数据都是十六进制数形式的字符（0~~F），其中A~~F是大写字母
text有基础值，二进制16*16的形式就是个棋盘：

1011111011110101
1000101110111100
1010000011101001
0111001100010000
1101100100010000
1010001110101101
1100110010110110
0100110111011110
0011010001001100
0011101111010110
0110011100010001
1000011010001111
0001110001111010
1000010000100101
0110101100001101
0001101101001100
读入的数据，（从0开始）奇数位表示行，偶数位表示列，每两个数一组组成要改变状态的棋子的位置
最后判断棋盘是否全为1，全为1即正确

分析的一些小坑

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[] != 找到的解))来实现

下面是完整的脚本：

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(跑出来的结果)}

updated at 2021-03-15

# wp # z3 # V&N2021

filpgame

程序分析

分析的一些小坑

exp

Comments