0x00 ez_rev

常规查壳 64位无壳ELF文件

5aa15ad2fd94e778ab47d5832f284a2.png

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
__int64 __fastcall main(int a1, char **a2, char **a3)
{
  char *v4; // rbx
  __int128 *v5; // rdx
  char *v6; // rdi
  __int64 v7; // rdx

  puts("Input:");
  __isoc99_scanf("%s", &dword_40A0);
  if ( dword_40A0 == 1179927374 && byte_40A4 == 123 && byte_40C9 == 125 && !byte_40CA )
  {
    v4 = (char *)&unk_40A5;
    v5 = &xmmword_40E0;
    do
    {
      v6 = v4;
      v4 += 4;
      sub_1290(v6, &unk_4060, v5);
      v5 = (__int128 *)(v7 + 4);
    }
    while ( v4 != (char *)&unk_40A5 + 36 );
  }
  if ( xmmword_40E0 == xmmword_4020 && xmmword_40F0 == xmmword_4030 && dword_4040 == dword_4100 )
    __printf_chk(1LL, "Right!");
  return 0LL;
}

简单分析一下主函数

定位到最后的判断语句，查看数据

312abcf927e8f0ce61a8976383d3f32.png

按“D”键将其转化为数值

8fe422d8c6afe9bab799c7df410639e.png

再定位到主函数中间的加密函数sub_1290

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
__int64 __fastcall sub_1290(unsigned __int8 *a1, char *a2, _BYTE *a3)
{
  int v3; // ebx
  unsigned __int8 v4; // r8
  char v5; // r10
  int v6; // er11
  unsigned __int8 v7; // al
  int v8; // ebp
  unsigned __int8 v9; // r9
  char v10; // cl
  char v11; // si
  char v12; // di
  char v13; // al
  char v14; // si
  char v15; // r8
  __int64 result; // rax

  v3 = (unsigned __int8)a2[3];
  v4 = a1[3];
  v5 = *a2;
  v6 = *a1;
  v7 = a1[1];
  v8 = (unsigned __int8)a2[1];
  v9 = a1[2];
  v10 = (v6 + v4) * (*a2 + v3);
  v11 = a2[2];
  v12 = v3 * (v6 + v7);
  v13 = (v3 + v11) * (v7 - v4);
  v14 = v4 * (v11 - v5);
  v15 = v5 * (v9 + v4);
  *a3 = v14 + v10 + v13 - v12;
  a3[2] = v15 + v14;
  result = (unsigned int)(v6 * (v8 - v3));
  a3[1] = v6 * (v8 - v3) + v12;
  a3[3] = v6 * (v8 - v3) + (v8 + v5) * (v9 - v6) + v10 - v15;
  return result;
}

简单分析一下是一个类似方程组的加密

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

m = [0x7A, 0x08, 0x2E, 0xBA, 0xAD, 0xAF, 0x82, 0x8C, 0xEF, 0xD8,
0x0D, 0xF8, 0x99, 0xEB, 0x2A, 0x16, 0x05, 0x43, 0x9F, 0xC8,
0x6D, 0x0A, 0x7F, 0xBE, 0x76, 0x64, 0x2F, 0xA9, 0xAC, 0xF2,
0xC9, 0x47, 0x75, 0x75, 0xB5, 0x33]

key = [0x7E, 0x1F, 0x19, 0x75]

flag = ''

for j in range(9):
s = Solver()
a = [BitVec(f"a[{i}]",16)for i in range(4)]
# x,y,z,k = Ints("x y z k")
s.add(m[4*j] == (a[3]*(key[2]-key[0]) + (a[0]+a[3])*(key[0]+key[3]) + (key[3
s.add(m[4*j+2] == (key[0]*(a[2]+a[3]) + a[3]*(key[2]-key[0])) & 0xff)
s.add(m[4*j+1] == (a[0]*(key[1]-key[3]) + key[3]*(a[0]+a[1])) & 0xff)
s.add(m[4*j+3] == (a[0]*(key[1]-key[3]) + (key[1]+key[0])*(a[2]-a[0]) + (a[0
# print(s.check())
assert s.check() == z3.sat
solve1 = s.model()
flag += "".join([chr(solve1.eval(j).as_long()) for j in a])
print(flag)