0x00 前言

试试爆破和klee两种方法

0x01 解

分析

无壳，64位，直接上IDA

还算简洁，就是注意输入中间每隔几位就要用-隔开，要不然读不到

先看看sub_401550

AES，没啥好说的，sub_401BCE是轮密钥加，sub_4016FD是字节代换，sub_4017C5是行移位，sub_40197E是列混合

可以在字节代换里面找到S盒，流程是标准的AES流程，没魔改，解密时可以直接解密

key是调用AES时的第二个参数unk_405420，共16Bytes

1
0x35, 0x77, 0x40, 0x2E, 0xCC, 0xA4, 0x4A, 0x3F, 0x9A, 0xB7, 0x21, 0x82, 0xF9, 0xB0, 0x1F, 0x35

之后才是重量级

AES的加密结果丢进了这个函数，a2就是丢进来的值，a1就是转换结果

分析了一下，a1总共16*12Bytes长，每12Bytes为一个单元，一个单元分为两个部分，第一个部分为a1[11]a1[8]，分别存入1或0，应该是序号，最多为15（即F），而第二部分为a1[7]a1[0]，存入的是a2的内容，一个一个位存（即将a2从十六进制分解成了二进制）

最后一个比较函数，看到下面一长串约束就感觉得上Z3了，但是比较鸡贼的地方是z3识别不了约束中间的判断操作（如表达式v11 == 0不会有返回值，而是直接当成约束）

爆破

跟他爆了！注意一下低位的索引最大，且要分成两部分

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
f = []
for i in range(16):
    b11 = int(i&0x1 == 1)
    b10 = int(i&0x2 == 2)
    b9 = int(i&0x4 == 4)
    b8 = int(i&0x8 == 8)
    for j in range(256):
        b0 = ((j>>7)&1)
        b1 = ((j>>6)&1)
        b2 = ((j>>5)&1)
        b3 = ((j>>4)&1)
        b4 = ((j>>3)&1)
        b5 = ((j>>2)&1)
        b6 = ((j>>1)&1)
        b7 = ((j>>0)&1)
        v1 = b9 & b8 & b7 & (b5 == 0) & (b4 == 0) & b3 & ((b2 | b1 | b0) == 0) & (b6 == 0) & (b10 == 0) | b9 & b7 & b5 & (b3 == 0) & (b2 == 0) & b0 & (b1 == 0) & (b4 == 0) & (b6 == 0) & (b8 == 0) & (b10 == 0) | b10 & (b8 == 0) & (b7 == 0) & (b6 == 0) & b5 & b4 & (b2 & b1 & b0) & (b3 == 0) & (b9 == 0)
        v2 = b11 & b10 & b8 & b7 & b6 & b5 & b4 & (b2 == 0) & (b1 & b0) & (b3 == 0) & (b9 == 0) | (b10 == 0) & (b9 == 0) & b8 & b7 & b6 & b4 & b3 & b1 & (b0 == 0) & (b2 == 0) & (b5 == 0) & (b11 == 0) | b11 & (b9 == 0) & b8 & b6 & b4 & b3 & b2 & b0 & (b1 == 0) & (b5 == 0) & (b7 == 0) & (b10 == 0) | b11 & b9 & b8 & b6 & b5 & b3 & b2 & (b1 == 0) & (b4 == 0) & (b7 == 0) & (b10 == 0) | (v1 | b10 & b9 & (b7 == 0) & b6 & (b4 == 0) & b3 & b2 & b0 & (b1 == 0) & (b5 == 0) & (b8 == 0)) & (b11 == 0)
        v3 = b11 & b10 & (b8 == 0) & (b7 == 0) & b6 & (b4 == 0) & (b3 == 0) & (b2 == 0) & (b1 & b0) & (b5 == 0) & (b9 == 0) | (b10 == 0) & (b9 == 0) & (b8 == 0) & (b7 == 0) & b6 & (b4 == 0) & b3 & ((b2 | b1 | b0) == 0) & (b5 == 0) & (b11 == 0) | b11 & b10 & b9 & (b7 == 0) & (b6 == 0) & b5 & b4 & (b2 == 0) & b1 & (b0 == 0) & (b3 == 0) & (b8 == 0) | b11 & b9 & (b7 == 0) & (b6 == 0) & b5 & ((b4 | b3 | b2 | b1 | b0) == 0) & (b8 == 0) & (b10 == 0) | b11 & (b9 == 0) & (b8 == 0) & b7 & b6 & b5 & b4 & (b2 == 0) & b0 & (b1 == 0) & (b3 == 0) & (b10 == 0) | v2
        if (b10 & b8 & b6 & b4 & (b2 == 0) & b1 & (b0 == 0) & (b3 == 0) & (b5 == 0) & (b7 == 0) & (b9 == 0) & (b11 == 0) | b11 & b10 & b9 & b8 & (b6 == 0) & (b5 == 0) & b4 & (b2 == 0) & b1 & (b0 == 0) & (b3 == 0) & (b7 == 0) | v3 | b10 & b9 & b8 & b6 & b4 & ((b3 | b2 | b1 | b0) == 0) & (b5 == 0) & (b7 == 0) & (b11 == 0))==1:
            print(j)
            f.append(j)
            break	# 别问，问就是爆出来发现有多解
for i in f:
    print("{:02X}".format(i),end=' ')
# 12 8F EC C2 85 04 B2 4C 5B BA 4A CF 11 36 0A 48

最后解一下AES加上-就行

flag{4d87ef03-77bb-491a-80f5-4620245807c4}

KLEE

这边用个LazyKLEE方便操作

首先include一下defs.h（来自IDA的plugins文件夹）

然后将要解的SMT从IDA直接复制进来

最后在main函数里面调用KLEE相关函数

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

#include "defs.h"
#include "stdio.h"
unsigned char flag[16];

__int64  check(_DWORD *a1)
{
  int v1; // r8d
  int v2; // ecx
  int v3; // ecx
  int v5; // [rsp+8h] [rbp-38h]
  int v6; // [rsp+Ch] [rbp-34h]
  int v7; // [rsp+10h] [rbp-30h]
  int v8; // [rsp+14h] [rbp-2Ch]
  int v9; // [rsp+18h] [rbp-28h]
  int v10; // [rsp+1Ch] [rbp-24h]
  int v11; // [rsp+20h] [rbp-20h]
  int v12; // [rsp+24h] [rbp-1Ch]
  int v13; // [rsp+28h] [rbp-18h]
  int v14; // [rsp+2Ch] [rbp-14h]
  __int64 v15; // [rsp+30h] [rbp-10h]
  int i; // [rsp+38h] [rbp-8h]
  unsigned int v17; // [rsp+3Ch] [rbp-4h]

  v17 = 1;
  for ( i = 0; i <= 15; ++i )
  {
    HIDWORD(v15) = a1[12 * i];
    LODWORD(v15) = a1[12 * i + 1];
    v14 = a1[12 * i + 2];
    v13 = a1[12 * i + 3];
    v12 = a1[12 * i + 4];
    v11 = a1[12 * i + 5];
    v10 = a1[12 * i + 6];
    v9 = a1[12 * i + 7];
    v8 = a1[12 * i + 8];
    v7 = a1[12 * i + 9];
    v6 = a1[12 * i + 10];
    v5 = a1[12 * i + 11];
    v1 = (unsigned __int8)v7 & (unsigned __int8)v8 & (unsigned __int8)v9 & (v11 == 0) & (v12 == 0) & (unsigned __int8)v13 & ((v14 | (unsigned int)v15 | HIDWORD(v15)) == 0) & (v10 == 0) & (v6 == 0) | (unsigned __int8)v7 & (unsigned __int8)v9 & (unsigned __int8)v11 & (v13 == 0) & (v14 == 0) & BYTE4(v15) & ((_DWORD)v15 == 0) & (v12 == 0) & (v10 == 0) & (v8 == 0) & (v6 == 0) | (unsigned __int8)v6 & (v8 == 0) & (v9 == 0) & (v10 == 0) & (unsigned __int8)v11 & (unsigned __int8)v12 & (unsigned __int8)(v14 & v15 & BYTE4(v15)) & (v13 == 0) & (v7 == 0);
    v2 = (unsigned __int8)v5 & (unsigned __int8)v6 & (unsigned __int8)v8 & (unsigned __int8)v9 & (unsigned __int8)v10 & (unsigned __int8)v11 & (unsigned __int8)v12 & (v14 == 0) & (unsigned __int8)(v15 & BYTE4(v15)) & (v13 == 0) & (v7 == 0) | (v6 == 0) & (v7 == 0) & (unsigned __int8)v8 & (unsigned __int8)v9 & (unsigned __int8)v10 & (unsigned __int8)v12 & (unsigned __int8)v13 & (unsigned __int8)v15 & (HIDWORD(v15) == 0) & (v14 == 0) & (v11 == 0) & (v5 == 0) | (unsigned __int8)v5 & (v7 == 0) & (unsigned __int8)v8 & (unsigned __int8)v10 & (unsigned __int8)v12 & (unsigned __int8)v13 & (unsigned __int8)v14 & BYTE4(v15) & ((_DWORD)v15 == 0) & (v11 == 0) & (v9 == 0) & (v6 == 0) | (unsigned __int8)v5 & (unsigned __int8)v7 & (unsigned __int8)v8 & (unsigned __int8)v10 & (unsigned __int8)v11 & (unsigned __int8)v13 & (unsigned __int8)v14 & (v15 == 0) & (v12 == 0) & (v9 == 0) & (v6 == 0) | (v1 | (unsigned __int8)v6 & (unsigned __int8)v7 & (v9 == 0) & (unsigned __int8)v10 & (v12 == 0) & (unsigned __int8)v13 & (unsigned __int8)v14 & BYTE4(v15) & ((_DWORD)v15 == 0) & (v11 == 0) & (v8 == 0)) & (v5 == 0);
    v3 = (unsigned __int8)v5 & (unsigned __int8)v6 & (v8 == 0) & (v9 == 0) & (unsigned __int8)v10 & (v12 == 0) & (v13 == 0) & (v14 == 0) & (unsigned __int8)(v15 & BYTE4(v15)) & (v11 == 0) & (v7 == 0) | (v6 == 0) & (v7 == 0) & (v8 == 0) & (v9 == 0) & (unsigned __int8)v10 & (v12 == 0) & (unsigned __int8)v13 & ((v14 | (unsigned int)v15 | HIDWORD(v15)) == 0) & (v11 == 0) & (v5 == 0) | (unsigned __int8)v5 & (unsigned __int8)v6 & (unsigned __int8)v7 & (v9 == 0) & (v10 == 0) & (unsigned __int8)v11 & (unsigned __int8)v12 & (v14 == 0) & (unsigned __int8)v15 & (HIDWORD(v15) == 0) & (v13 == 0) & (v8 == 0) | (unsigned __int8)v5 & (unsigned __int8)v7 & (v9 == 0) & (v10 == 0) & (unsigned __int8)v11 & ((v12 | v13 | v14 | (unsigned int)v15 | HIDWORD(v15)) == 0) & (v8 == 0) & (v6 == 0) | (unsigned __int8)v5 & (v7 == 0) & (v8 == 0) & (unsigned __int8)v9 & (unsigned __int8)v10 & (unsigned __int8)v11 & (unsigned __int8)v12 & (v14 == 0) & BYTE4(v15) & ((_DWORD)v15 == 0) & (v13 == 0) & (v6 == 0) | v2;
    if ( !((unsigned __int8)v6 & (unsigned __int8)v8 & (unsigned __int8)v10 & (unsigned __int8)v12 & (v14 == 0) & (unsigned __int8)v15 & (HIDWORD(v15) == 0) & (v13 == 0) & (v11 == 0) & (v9 == 0) & (v7 == 0) & (v5 == 0) | (unsigned __int8)v5 & (unsigned __int8)v6 & (unsigned __int8)v7 & (unsigned __int8)v8 & (v10 == 0) & (v11 == 0) & (unsigned __int8)v12 & (v14 == 0) & (unsigned __int8)v15 & (HIDWORD(v15) == 0) & (v13 == 0) & (v9 == 0) | v3 | (unsigned __int8)v6 & (unsigned __int8)v7 & (unsigned __int8)v8 & (unsigned __int8)v10 & (unsigned __int8)v12 & ((v13 | v14 | (unsigned int)v15 | HIDWORD(v15)) == 0) & (v11 == 0) & (v9 == 0) & (v5 == 0)) )
      v17 = 0;
  }
  return v17;
}

void  trans(_DWORD *a1, unsigned char *dst)
{
  __int64 v2; // rax
  int k; // [rsp+0h] [rbp-10h]
  int j; // [rsp+4h] [rbp-Ch]
  int i; // [rsp+8h] [rbp-8h]
  int v7; // [rsp+Ch] [rbp-4h]

  for ( i = 0; i <= 15; ++i )
  {
    LOBYTE(v2) = i;
    v7 = i;
    for ( j = 0; j <= 3; ++j )
    {
      v2 = 11 - j;
      a1[12 * i + v2] = v7 & 1;
      v7 >>= 1;
    }
    for ( k = 0; k <= 7; ++k )
    {
      a1[12 * i + 7 - k] = dst[i] & 1;
      LOBYTE(v2) = (unsigned __int8)dst[i] >> 1;
      dst[i] = v2;
    }
  }
  return ;
}
int  main(int argc, const char **argv, const char **envp)
{
    klee_make_symbolic(flag, sizeof(flag), "buf");
    _DWORD tmp[192];	// 数组给个大小就行（甚至不用初始化）
    trans(tmp, flag);
    if(check(tmp))		// 来个判断条件
    {
        printf("Good Job.\n");
        klee_assert(0);	// 表示结束
    }
  return 0;
}

最后用命令

1
python LazyKLEE.py [srcname]

就可以喝茶等结果了

（有一说一挺慢的，不知道是不是因为在虚拟机里面跑，或许在实机跑会快点？）