AVALON 零散的一些题目 网鼎杯CTF Martricks

网鼎杯CTF Martricks

环境配置

系统 : Linux kali 4.6.0-kali1-amd64
程序 : 1.1
要求 : 输入口令
使用工具 :ida \ angr \ z3

解法一

主要流程

使用ida了解程序结构如下:

__int64 __fastcall main(__int64 a1, char **a2, char **a3)
{
  unsigned __int8 v4; // [rsp+Bh] [rbp-E5h]
  signed int v5; // [rsp+Ch] [rbp-E4h]
  signed int v6; // [rsp+10h] [rbp-E0h]
  int v7; // [rsp+14h] [rbp-DCh]
  signed int v8; // [rsp+18h] [rbp-D8h]
  signed int v9; // [rsp+1Ch] [rbp-D4h]
  int v10; // [rsp+1Ch] [rbp-D4h]
  int v11; // [rsp+20h] [rbp-D0h]
  int i; // [rsp+20h] [rbp-D0h]
  int v13; // [rsp+24h] [rbp-CCh]
  int v14; // [rsp+28h] [rbp-C8h]
  signed int v15; // [rsp+2Ch] [rbp-C4h]
  char v16[56]; // [rsp+B0h] [rbp-40h]
  unsigned __int64 v17; // [rsp+E8h] [rbp-8h]
  __int64 savedregs; // [rsp+F0h] [rbp+0h]

  v17 = __readfsqword(0x28u);
  puts("input your flag:");
  __isoc99_scanf("%49s", v16);
  v15 = 1;
  v9 = 0;
  v11 = 23;
  while ( v9 <= 48 )
  {
    *((_BYTE *)&savedregs + 7 * (v11 / 7) + v11 % 7 - 192) = v16[v9] ^ v11;
    *((_BYTE *)&savedregs + 7 * (v9 / 7) + v9 % 7 - 128) = byte_601060[v11] ^ v9;
    ++v9;
    v11 = (v11 + 13) % 49;
  }
  v10 = 41;
  v13 = 3;
  v14 = 4;
  v7 = 5;
  v5 = 0;
  while ( v5 <= 6 && v15 )
  {
    v6 = 0;
    while ( v6 <= 6 && v15 )
    {
      v4 = 0;
      v8 = 0;
      while ( v8 <= 6 )
      {
        v4 += *((_BYTE *)&savedregs + 7 * v7 + v14 - 128) * *((_BYTE *)&savedregs + 7 * v13 + v7 - 192);
        ++v8;
        v7 = (v7 + 5) % 7;
      }
      for ( i = 17; i != v10; i = (i + 11) % 49 )
        ;
      if ( byte_6010A0[7 * (i / 7) + i % 7] != ((unsigned __int8)i ^ v4) )
        v15 = 0;
      v10 = (v10 + 31) % 49;
      ++v6;
      v14 = (v14 + 4) % 7;
    }
    ++v5;
    v13 = (v13 + 3) % 7;
  }
  if ( v15 )
    puts("congrats!");
  else
    puts("wrong flag!");
  return 0LL;
}

定位到判断语句:

.text:0000000000400A7B loc_400A7B:                             ; CODE XREF: main+476↑j
.text:0000000000400A7B                 cmp     [rbp+var_C4], 0
.text:0000000000400A82                 jz      short loc_400A90
.text:0000000000400A84                 mov     edi, offset aCongrats ; "congrats!"
.text:0000000000400A89                 call    _puts
.text:0000000000400A8E                 jmp     short loc_400A9A
.text:0000000000400A90 ; ---------------------------------------------------------------------------
.text:0000000000400A90
.text:0000000000400A90 loc_400A90:                             ; CODE XREF: main+48C↑j
.text:0000000000400A90                 mov     edi, offset aWrongFlag ; "wrong flag!"
.text:0000000000400A95                 call    _puts

编写脚本

使用angr安排程序算法:

import angr

proj = angr.Project("1.1",auto_load_libs=False)
sm = proj.factory.simulation_manager(proj.factory.entry_state())
found = sm.explore(find = 0x400A84,avoid = 0x400A90).found[0]
print found.posix.dumps(0)

运行一分钟后输出:

(angr) ➜  playground python 1_1.py
WARNING | 2019-04-29 04:09:24,529 | angr.analyses.disassembly_utils | Your version of capstone does not support MIPS instruction groups.
flag{Everyth1n_th4t_kill5_m3_m4kes_m3_fee1_aliv3}

解法二

美化结构

重命名变量名之后程序如下:

__int64 __fastcall main(__int64 a1, char **a2, char **a3)
{
  unsigned __int8 sum; // [rsp+Bh] [rbp-E5h]
  signed int index_i; // [rsp+Ch] [rbp-E4h]
  signed int index_j; // [rsp+10h] [rbp-E0h]
  int offest_3; // [rsp+14h] [rbp-DCh]
  signed int index_k; // [rsp+18h] [rbp-D8h]
  signed int index; // [rsp+1Ch] [rbp-D4h]
  int offest_0; // [rsp+1Ch] [rbp-D4h]
  int xor_data; // [rsp+20h] [rbp-D0h]
  int xor_index_data; // [rsp+20h] [rbp-D0h]
  int offest_1; // [rsp+24h] [rbp-CCh]
  int offest_2; // [rsp+28h] [rbp-C8h]
  signed int res; // [rsp+2Ch] [rbp-C4h]
  char my_str[56]; // [rsp+B0h] [rbp-40h]
  unsigned __int64 v17; // [rsp+E8h] [rbp-8h]
  __int64 savedregs; // [rsp+F0h] [rbp+0h]

  v17 = __readfsqword(0x28u);
  puts("input your flag:");
  __isoc99_scanf("%49s", my_str);
  res = 1;
  index = 0;
  xor_data = 23;
  while ( index <= 48 )
  {
    *(&savedregs + 7 * (xor_data / 7) + xor_data % 7 - 192) = my_str[index] ^ xor_data;// data_area_192 = xored_input
    *(&savedregs + 7 * (index / 7) + index % 7 - 128) = aSomeLegendsRTo[xor_data] ^ index;// data_area_128 = changed_hardcode
    ++index;
    xor_data = (xor_data + 13) % 49;
  }
  offest_0 = 0x29;
  offest_1 = 3;
  offest_2 = 4;
  offest_3 = 5;
  index_i = 0;
  while ( index_i <= 6 && res )
  {
    index_j = 0;
    while ( index_j <= 6 && res )
    {
      sum = 0;
      index_k = 0;
      while ( index_k <= 6 )
      {
        sum += *(&savedregs + 7 * offest_3 + offest_2 - 128) * *(&savedregs + 7 * offest_1 + offest_3 - 192);
        ++index_k;
        offest_3 = (offest_3 + 5) % 7;
      }
      for ( xor_index_data = 17; xor_index_data != offest_0; xor_index_data = (xor_index_data + 11) % 0x31 )
        ;
      if ( byte_6010A0[7 * (xor_index_data / 7) + xor_index_data % 7] != (xor_index_data ^ sum) )
        res = 0;
      offest_0 = (offest_0 + 31) % 49;
      ++index_j;
      offest_2 = (offest_2 + 4) % 7;
    }
    ++index_i;
    offest_1 = (offest_1 + 3) % 7;
  }
  if ( res )
    puts("congrats!");
  else
    puts("wrong flag!");
  return 0LL;
}

逻辑推理

程序在模拟矩阵相乘,两个7*7的矩阵相乘,最后与固定值对比,由于采取了比较迷的值作为数组的索引值,这里我们可以使用z3约束求解器来计算flag。

编写脚本

python照抄一遍,用z3求解:

from z3 import *
byte_610a0 = [0xAA, 0x7A, 0x24, 0x0A, 0xA8, 0xBC, 0x3C, 0xFC, 0x82, 0x4B, 0x51, 0x52, 0x5E, 0x1C, 0x82, 0x1F, 0x79, 0xBA, 0xB5, 0xE3, 0x43, 0x04, 0xFD, 0xAC, 0x10, 0xB5, 0x63, 0xBD, 0x8D, 0xE7, 0x35, 0xD9, 0xD3, 0xE8, 0x42, 0x6D, 0x71, 0x5A, 0x09, 0x54, 0xE9, 0x9F, 0x4C, 0xDC, 0xA2, 0xAF, 0x11, 0x87, 0x94] 
byte_601060 = [0x73,0x6F,0x6D,0x65,0x20,0x6C,0x65,0x67,0x65,0x6E,0x64,0x73,0x20,0x72,0x20,0x74,0x6F,0x6C,0x64,0x2C,0x20,0x73,0x6F,0x6D,0x65,0x20,0x74,0x75,0x72,0x6E,0x20,0x74,0x6F,0x20,0x64,0x75,0x73,0x74,0x20,0x6F,0x72,0x20,0x74,0x6F,0x20,0x67,0x6F,0x6C,0x64]

flag = [BitVec("flag%d"%i,8) for i in range(49)]
m1 = [0 for i in range(49)]
m2 = [0 for i in range(49)]

xor_data = 23
for index in range(49):
    m1[xor_data] = flag[index] ^ xor_data
    m2[index] = byte_601060[xor_data] ^ index
    xor_data = (xor_data + 13) % 49

offest_0 = 0x29
offest_1 = 3
offest_2 = 4
offest_3 = 5

solver = Solver()

for index_i in range(7):
    for index_j in range(7):
        sum = 0
        for index_k in range(7):
            sum += m2[7*offest_3+offest_2] * m1[7*offest_1+offest_3]
            offest_3 = (offest_3 + 5) % 7
        xor_index_data = offest_0
        solver.add(sum^xor_index_data == byte_610a0[xor_index_data])
        offest_0 = (offest_0 + 31) % 49
        offest_2 = (offest_2 + 4) % 7
    offest_1 = (offest_1 + 3) % 7

f = ""
if ( solver.check() == sat ):
    m = solver.model()
    for i in range(49):
        f += (chr(m[flag[i]].as_long()))
    print f

夺旗成功

输入获得的flag,程序提示成功:

➜  playground ./1.1
input your flag:
flag{Everyth1n_th4t_kill5_m3_m4kes_m3_fee1_aliv3}
congrats!

参考链接

  1. angr学习【一】 https://blog.csdn.net/qq_33438733/article/details/80276628
  2. Z3 学习笔记 https://blog.csdn.net/qq_33438733/article/details/82011892
  3. 180822 逆向-网鼎杯(2-1)https://blog.csdn.net/whklhhhh/article/details/81950438