伪代码分析

signed __int64 __fastcall main(int a1, char **a2, char **a3)
{
  signed __int64 result; // rax
  char *j; // rax
  char v5; // ST1F_1
  char v6; // ST1E_1
  char v7; // [rsp+1Dh] [rbp-1B3h]
  signed int i; // [rsp+20h] [rbp-1B0h]
  signed int k; // [rsp+24h] [rbp-1ACh]
  int v10; // [rsp+28h] [rbp-1A8h]
  int v11; // [rsp+2Ch] [rbp-1A4h]
  signed int l; // [rsp+30h] [rbp-1A0h]
  signed int m; // [rsp+34h] [rbp-19Ch]
  int v14; // [rsp+38h] [rbp-198h]
  int v15; // [rsp+3Ch] [rbp-194h]
  signed int n; // [rsp+40h] [rbp-190h]
  signed int ii; // [rsp+44h] [rbp-18Ch]
  int v18; // [rsp+48h] [rbp-188h]
  signed int jj; // [rsp+4Ch] [rbp-184h]
  char *s; // [rsp+58h] [rbp-178h]
  __int64 v21; // [rsp+70h] [rbp-160h]
  __int64 v22; // [rsp+78h] [rbp-158h]
  __int64 v23; // [rsp+80h] [rbp-150h]
  __int64 v24; // [rsp+88h] [rbp-148h]
  __int64 v25; // [rsp+90h] [rbp-140h]
  __int64 v26; // [rsp+98h] [rbp-138h]
  __int64 v27; // [rsp+A0h] [rbp-130h]
  __int64 v28; // [rsp+A8h] [rbp-128h]
  __int64 v29; // [rsp+B0h] [rbp-120h]
  __int64 v30; // [rsp+B8h] [rbp-118h]
  __int64 v31; // [rsp+C0h] [rbp-110h]
  __int64 v32; // [rsp+C8h] [rbp-108h]
  __int64 v33; // [rsp+D0h] [rbp-100h]
  __int64 v34; // [rsp+D8h] [rbp-F8h]
  __int64 v35; // [rsp+E0h] [rbp-F0h]
  __int64 v36; // [rsp+E8h] [rbp-E8h]
  __int64 s1; // [rsp+F0h] [rbp-E0h]
  __int64 v38; // [rsp+F8h] [rbp-D8h]
  __int64 v39; // [rsp+100h] [rbp-D0h]
  __int64 v40; // [rsp+108h] [rbp-C8h]
  __int64 v41; // [rsp+110h] [rbp-C0h]
  __int64 v42; // [rsp+118h] [rbp-B8h]
  __int64 v43; // [rsp+120h] [rbp-B0h]
  __int64 v44; // [rsp+128h] [rbp-A8h]
  int v45[32]; // [rsp+130h] [rbp-A0h]
  __int64 v46; // [rsp+1B0h] [rbp-20h]
  __int64 v47; // [rsp+1B8h] [rbp-18h]
  unsigned __int64 v48; // [rsp+1C8h] [rbp-8h]

  v48 = __readfsqword(0x28u);
  if ( a1 == 2 )
  {
    s = a2[1];
    if ( strlen(a2[1]) != 39 )
    {
      puts("incorrect");
      exit(0);
    }
    if ( memcmp(s, "TWCTF{", 6uLL) || s[38] != '}' )
    {
      puts("incorrect");
      exit(0);
    }
    s1 = 0LL;
    v38 = 0LL;
    v39 = 0LL;
    v40 = 0LL;
    v41 = 0LL;
    v42 = 0LL;
    v43 = 0LL;
    v44 = 0LL;
    v46 = '76543210';
    v47 = 'fedcba98';                           // 判断字符出现的次数
    for ( i = 0; i <= 15; ++i )
    {
      for ( j = strchr(s, *(&v46 + i)); j; j = strchr(j + 1, *(&v46 + i)) )
        ++*(&s1 + i);
    }
    if ( memcmp(&s1, &dword_400F00, 0x40uLL) )
    {
      puts("incorrect");
      exit(0);
    }
    v21 = 0LL;
    v22 = 0LL;
    v23 = 0LL;
    v24 = 0LL;
    v25 = 0LL;
    v26 = 0LL;
    v27 = 0LL;
    v28 = 0LL;
    for ( k = 0; k <= 7; ++k )                  // 操作中间的32位 每4位一组
    {
      v10 = 0;
      v11 = 0;
      for ( l = 0; l <= 3; ++l )
      {
        v5 = s[4 * k + 6 + l];
        v10 += v5;
        v11 ^= v5;
      }
      *(&v21 + k) = v10;
      *(&v25 + k) = v11;
    }
    v29 = 0LL;
    v30 = 0LL;
    v31 = 0LL;
    v32 = 0LL;
    v33 = 0LL;
    v34 = 0LL;
    v35 = 0LL;
    v36 = 0LL;
    for ( m = 0; m <= 7; ++m )
    {
      v14 = 0;
      v15 = 0;
      for ( n = 0; n <= 3; ++n )
      {
        v6 = s[8 * n + 6 + m];                  // 6 14 22 30
        v14 += v6;                              // 7 15 23 31
        v15 ^= v6;                              // 8 16 24 32
      }
      *(&v29 + m) = v14;
      *(&v33 + m) = v15;
    }
    if ( memcmp(&v21, &dword_400F40, 0x20uLL) || memcmp(&v25, &dword_400F60, 0x20uLL) )// 对比
    {
      puts("incorrect");
      exit(0);
    }
    if ( memcmp(&v29, &dword_400FA0, 0x20uLL) || memcmp(&v33, &unk_400F80, 0x20uLL) )// 对比
    {
      puts("incorrect");
      exit(0);
    }
    memset(v45, 0, sizeof(v45));
    for ( ii = 0; ii <= 31; ++ii )              // 通过中间32位 产生v45
    {
      v7 = s[ii + 6];
      if ( v7 <= 47 || v7 > 57 )
      {
        if ( v7 <= '`' || v7 > 'f' )
          v45[ii] = 0;
        else
          v45[ii] = 128;
      }
      else
      {
        v45[ii] = 255;
      }
    }
    if ( memcmp(v45, &unk_400FC0, 0x80uLL) )
    {
      puts("incorrect");
      exit(0);
    }
    v18 = 0;
    for ( jj = 0; jj <= 15; ++jj )              // 6 8 10 12 14
      v18 += s[2 * (jj + 3)];
    if ( v18 != 1160 )
    {
      puts("incorrect");
      exit(0);
    }
    if ( s[37] != '5' || s[7] != 'f' || s[11] != '8' || s[12] != '7' || s[23] != '2' || s[31] != '4' )
    {
      puts("incorrect");
      exit(0);
    }
    printf("Correct: %s\n", s, a2);
    result = 0LL;
  }
  else
  {
    fwrite("./bin flag_is_here", 1uLL, 0x12uLL, stderr);
    result = 1LL;
  }
  return result;
}

很明显可以使用z3求解器求解,但这里有个问题z3无法判断字符出现的次数,所以这里我使用z3进行暴力破解

暴力破解只存在一个的字符,如”a”,可以得到只有30位才能为”a”,以此类推,最大程度的限制求解器。

爆破循环

# 爆破1位
for i in range(0,32):
    if i == 1 or i == 5 or i == 6 or i == 17 or i == 25 or i == 31 or i == 13 or i == 30 or i == 2 or i == 7 or i == 9 or i == 19 or i == 28 or i == 18 or i == 21:
        continue
    sol(i,0)
# 爆破2位
for i in range(0,32):
    if i == 1 or i == 5 or i == 6 or i == 17 or i == 25 or i == 31 or i == 13 or i == 30 or i == 2 or i == 7 or i == 9 or i == 19 or i == 28 or i == 18 or i == 21:
        continue
    if i == 4 or i == 29:
        continue
    for j in range(0,32):
        if j == 1 or j == 5 or j == 6 or j == 17 or j == 25 or j == 31 or j == 13 or j == 30 or j == 2 or j == 7 or j == 9 or j == 19 or j == 28 or j == 18 or j == 21:
            continue
        if i == j:
            continue
        if j == 4 or j == 29:
            continue
        sol(i,j)

添加限制

# 爆破 循环
for i in range(0,len(s)):
  if i == buf or i == buf1 or i == buf2:
    solver.add(s[i] == ord('b'))
  else:
    solver.add(s[i] != ord('b'))

最终可以得到

# 每个字符出现的次数
##       0    1    2    3    4    5    6    7    8    9    a    b    c    d    e    f
#num = [0x3, 0x2, 0x2, 0x0, 0x3, 0x2, 0x1, 0x3, 0x3, 0x1, 0x1, 0x3, 0x1, 0x2, 0x2, 0x3]
solver.add(s[1] == ord('f'))
solver.add(s[5] == ord('8'))
solver.add(s[6] == ord('7'))
solver.add(s[17] == ord('2'))
solver.add(s[25] == ord('4'))
solver.add(s[31] == ord('5'))

# 爆破一位
solver.add(s[13] == ord('9'))
for i in range(len(numorchar)):
    if i != 13:
        solver.add(s[i] != ord('9'))
solver.add(s[30] == ord('a'))
for i in range(len(numorchar)):
    if i != 30:
        solver.add(s[i] != ord('a'))
solver.add(s[2] == ord('2'))
for i in range(len(numorchar)):
    if i != 2 and i != 17:
        solver.add(s[i] != ord('2'))

# 爆破二位
solver.add(s[7] == ord('7'))
solver.add(s[9] == ord('7'))
for i in range(len(numorchar)):
    if i != 6 and i != 7 and i!=9:
        solver.add(s[i] != ord('7'))

solver.add(s[19] == ord('8'))
solver.add(s[28] == ord('8'))
for i in range(len(numorchar)):
    if i != 5 and i != 19 and i!=28:
        solver.add(s[i] != ord('8'))

solver.add(s[18] == ord('f'))
solver.add(s[21] == ord('f'))
for i in range(len(numorchar)):
    if i != 1 and i != 21 and i!=18:
        solver.add(s[i] != ord('f'))

solver.add(s[4] == ord('4'))
solver.add(s[29] == ord('4'))
for i in range(len(numorchar)):
    if i != 25 and i != 4 and i!=29:
        solver.add(s[i] != ord('4'))

# 剩下的一位和二位都是多解
# 6 在 22 27
# c 在 11 15
# 5 在 22 27

# 1 在 10 14
# 1 在 10 24
# 1 在 10 27
# 1 在 14 23

# d 在 0 12
# d 在 0 20

# e 在 8 12
# e 在 8 20
# e 在 11 12
# e 在 11 20

# 0 在 10 16 24
# 0 在 14 16 23
# 0 在 16 23 24
# 0 在 23 16 24

# b 在 3 11 26
# b 在 3 15 26

解密脚本

# -*- coding:utf8 -*-
# 使用z3约束求解
import z3
import sys
import time

start = time.time()
# 假设中间32位为 s
s = ['0' for i in range(0,32)]

nums = '0123456789abcdef'
# 每个字符出现的次数
#       0    1    2    3    4    5    6    7    8    9    a    b    c    d    e    f
num = [0x3, 0x2, 0x2, 0x0, 0x3, 0x2, 0x1, 0x3, 0x3, 0x1, 0x1, 0x3, 0x1, 0x2, 0x2, 0x3]

counts = 0
for i in range(0,len(num)):
    counts += ord(nums[i]) * num[i]

# 每四位一组相加结果
addfour = [0x15E, 0xDA, 0x12F, 0x131, 0x100, 0x131, 0xFB, 0x102]
# 每四位一组xor结果
xorfour = [0x52, 0xC, 0x1, 0xF, 0x5C, 0x5, 0x53, 0x58]

# 每隔八位相加结果
add = [0x129, 0x103, 0x12B, 0x131, 0x135, 0x10B, 0x0FF, 0x0FF]
# 每隔八位xor结果
xor = [0x1, 0x57, 0x7, 0xD, 0xD, 0x53, 0x51, 0x51]

# 为数字则为0xff 为字母则为128
numorchar = [0x80, 0x80, 0xFF, 0x80, 0xFF, 0xFF, 0xFF, 0xFF, 0x80, 0xFF, 0xFF, 0x80, 0x80, 0xFF, 0xFF, 0x80,0xFF, 0xFF, 0x80, 0xFF, 0x80, 0x80, 0xFF, 0xFF,0xFF, 0xFF, 0x80, 0xFF, 0xFF, 0xFF, 0x80, 0xFF]

# 每隔两位相加结果为1160
result = 1160

# s[37] != '5' || s[7] != 'f' || s[11] != '8' || s[12] != '7' || s[23] != '2' || s[31] != '4'

solver = z3.Solver()

for i in range(0,len(s)):
    s[i] = z3.BitVec('s[%d]'%i,8)

for i in range(0,len(addfour)):
    solver.add(s[i*4] + s[i*4+1] + s[i*4+2] + s[i*4+3] == addfour[i])
    solver.add(s[i*4] ^ s[i*4+1] ^ s[i*4+2] ^ s[i*4+3] == xorfour[i])

for i in range(0,len(add)):
    solver.add(s[i] + s[i+8] + s[i+16] + s[i+24] == add[i])
    solver.add(s[i] ^ s[i+8] ^ s[i+16] ^ s[i+24] == xor[i])

solver.add(s[0] + s[2] + s[4] + s[6] + s[8] + s[10] + s[12] + s[14] + s[16] + s[18] + s[20] + s[22] + s[24] + s[26] + s[28] + s[30] == result)
solver.add(s[1] + s[3] + s[5] + s[7] + s[9] + s[11] + s[13] + s[15] + s[17] + s[19] + s[21] + s[23] + s[25] + s[27] + s[29] + s[31] == counts-result)
solver.add(s[0] + s[1] + s[2] + s[3] + s[4] + s[5] + s[6] + s[7] + s[8] + s[9] + s[10] + s[11] + s[12] + s[13] + s[14] + s[15] + s[16] + s[17] + s[18] + s[19] + s[20] + s[21] + s[22] + s[23] + s[24] + s[25] + s[26] + s[27] + s[28] + s[29] + s[30] + s[31] == counts)

for i in range(len(numorchar)):
    if numorchar[i] == 0xff:
        solver.add(s[i] >= ord('0'))
        solver.add(s[i] <= ord('9'))
    else:
        solver.add(s[i] >= ord('a'))
        solver.add(s[i] <= ord('f'))
    solver.add(s[i] != ord('3'))

# 每个字符出现的次数
##       0    1    2    3    4    5    6    7    8    9    a    b    c    d    e    f
#num = [0x3, 0x2, 0x2, 0x0, 0x3, 0x2, 0x1, 0x3, 0x3, 0x1, 0x1, 0x3, 0x1, 0x2, 0x2, 0x3]
solver.add(s[1] == ord('f'))
solver.add(s[5] == ord('8'))
solver.add(s[6] == ord('7'))
solver.add(s[17] == ord('2'))
solver.add(s[25] == ord('4'))
solver.add(s[31] == ord('5'))

# 爆破一位
solver.add(s[13] == ord('9'))
for i in range(len(numorchar)):
    if i != 13:
        solver.add(s[i] != ord('9'))
solver.add(s[30] == ord('a'))
for i in range(len(numorchar)):
    if i != 30:
        solver.add(s[i] != ord('a'))
solver.add(s[2] == ord('2'))
for i in range(len(numorchar)):
    if i != 2 and i != 17:
        solver.add(s[i] != ord('2'))

# 爆破二位
solver.add(s[7] == ord('7'))
solver.add(s[9] == ord('7'))
for i in range(len(numorchar)):
    if i != 6 and i != 7 and i!=9:
        solver.add(s[i] != ord('7'))

solver.add(s[19] == ord('8'))
solver.add(s[28] == ord('8'))
for i in range(len(numorchar)):
    if i != 5 and i != 19 and i!=28:
        solver.add(s[i] != ord('8'))

solver.add(s[18] == ord('f'))
solver.add(s[21] == ord('f'))
for i in range(len(numorchar)):
    if i != 1 and i != 21 and i!=18:
        solver.add(s[i] != ord('f'))

solver.add(s[4] == ord('4'))
solver.add(s[29] == ord('4'))
for i in range(len(numorchar)):
    if i != 25 and i != 4 and i!=29:
        solver.add(s[i] != ord('4'))

# 剩下的一位和二位都是多解
# 6 在 22 27
# c 在 11 15
# 5 在 22 27

# 1 在 10 14
# 1 在 10 24
# 1 在 10 27
# 1 在 14 23

# d 在 0 12
# d 在 0 20

# e 在 8 12
# e 在 8 20
# e 在 11 12
# e 在 11 20

# 0 在 10 16 24
# 0 在 14 16 23
# 0 在 16 23 24
# 0 在 23 16 24

# b 在 3 11 26
# b 在 3 15 26

# 爆破 循环
#for i in range(0,len(s)):
#    if i == buf or i == buf1 or i == buf2:
#        solver.add(s[i] == ord('b'))
#    else:
#        solver.add(s[i] != ord('b'))

if solver.check() == z3.sat:
    solvers = solver.model()
    for i in range(0,len(solvers)):
        print(solvers[s[i]],",",end="")
# 100 ,102 ,50 ,98 ,52 ,56 ,55 ,55 ,101 ,55 ,49 ,98 ,100 ,57 ,49 ,99 ,48 ,50 ,102 ,56 ,101 ,102 ,54 ,48 ,48 ,52 ,98 ,53 ,56 ,52 ,97 ,53
# df2b4877e71bd91c02f8ef6004b584a5


reverse      writeup

本博客所有文章除特别声明外,均采用 CC BY-SA 3.0协议 。转载请注明出处!