z3

检查一下：

image-20200901230241645

IDA64打开：main函数

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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
// local variable allocation has failed, the output may be wrong!
int __cdecl main(int argc, const char **argv, const char **envp)
{
  int v4; // [rsp+20h] [rbp-60h]
  int v5; // [rsp+24h] [rbp-5Ch]
  int v6; // [rsp+28h] [rbp-58h]
  int v7; // [rsp+2Ch] [rbp-54h]
  int v8; // [rsp+30h] [rbp-50h]
  int v9; // [rsp+34h] [rbp-4Ch]
  int v10; // [rsp+38h] [rbp-48h]
  int v11; // [rsp+3Ch] [rbp-44h]
  int v12; // [rsp+40h] [rbp-40h]
  int v13; // [rsp+44h] [rbp-3Ch]
  int v14; // [rsp+48h] [rbp-38h]
  int v15; // [rsp+4Ch] [rbp-34h]
  int v16; // [rsp+50h] [rbp-30h]
  int v17; // [rsp+54h] [rbp-2Ch]
  int v18; // [rsp+58h] [rbp-28h]
  int v19; // [rsp+5Ch] [rbp-24h]
  int v20; // [rsp+60h] [rbp-20h]
  int v21; // [rsp+64h] [rbp-1Ch]
  int v22; // [rsp+68h] [rbp-18h]
  int v23; // [rsp+6Ch] [rbp-14h]
  int v24; // [rsp+70h] [rbp-10h]
  int v25; // [rsp+74h] [rbp-Ch]
  int v26; // [rsp+78h] [rbp-8h]
  int v27; // [rsp+7Ch] [rbp-4h]
  int v28; // [rsp+80h] [rbp+0h]
  int v29; // [rsp+84h] [rbp+4h]
  int v30; // [rsp+88h] [rbp+8h]
  int v31; // [rsp+8Ch] [rbp+Ch]
  int v32; // [rsp+90h] [rbp+10h]
  int v33; // [rsp+94h] [rbp+14h]
  int v34; // [rsp+98h] [rbp+18h]
  int v35; // [rsp+9Ch] [rbp+1Ch]
  int v36; // [rsp+A0h] [rbp+20h]
  int v37; // [rsp+A4h] [rbp+24h]
  int v38; // [rsp+A8h] [rbp+28h]
  int v39; // [rsp+ACh] [rbp+2Ch]
  int v40; // [rsp+B0h] [rbp+30h]
  int v41; // [rsp+B4h] [rbp+34h]
  int v42; // [rsp+B8h] [rbp+38h]
  int v43; // [rsp+BCh] [rbp+3Ch]
  int v44; // [rsp+C0h] [rbp+40h]
  int v45; // [rsp+C4h] [rbp+44h]
  unsigned __int8 v46; // [rsp+D0h] [rbp+50h]
  unsigned __int8 v47; // [rsp+D1h] [rbp+51h]
  unsigned __int8 v48; // [rsp+D2h] [rbp+52h]
  unsigned __int8 v49; // [rsp+D3h] [rbp+53h]
  unsigned __int8 v50; // [rsp+D4h] [rbp+54h]
  unsigned __int8 v51; // [rsp+D5h] [rbp+55h]
  unsigned __int8 v52; // [rsp+D6h] [rbp+56h]
  unsigned __int8 v53; // [rsp+D7h] [rbp+57h]
  unsigned __int8 v54; // [rsp+D8h] [rbp+58h]
  unsigned __int8 v55; // [rsp+D9h] [rbp+59h]
  unsigned __int8 v56; // [rsp+DAh] [rbp+5Ah]
  unsigned __int8 v57; // [rsp+DBh] [rbp+5Bh]
  unsigned __int8 v58; // [rsp+DCh] [rbp+5Ch]
  unsigned __int8 v59; // [rsp+DDh] [rbp+5Dh]
  unsigned __int8 v60; // [rsp+DEh] [rbp+5Eh]
  unsigned __int8 v61; // [rsp+DFh] [rbp+5Fh]
  unsigned __int8 v62; // [rsp+E0h] [rbp+60h]
  unsigned __int8 v63; // [rsp+E1h] [rbp+61h]
  unsigned __int8 v64; // [rsp+E2h] [rbp+62h]
  unsigned __int8 v65; // [rsp+E3h] [rbp+63h]
  unsigned __int8 v66; // [rsp+E4h] [rbp+64h]
  unsigned __int8 v67; // [rsp+E5h] [rbp+65h]
  unsigned __int8 v68; // [rsp+E6h] [rbp+66h]
  unsigned __int8 v69; // [rsp+E7h] [rbp+67h]
  unsigned __int8 v70; // [rsp+E8h] [rbp+68h]
  unsigned __int8 v71; // [rsp+E9h] [rbp+69h]
  unsigned __int8 v72; // [rsp+EAh] [rbp+6Ah]
  unsigned __int8 v73; // [rsp+EBh] [rbp+6Bh]
  unsigned __int8 v74; // [rsp+ECh] [rbp+6Ch]
  unsigned __int8 v75; // [rsp+EDh] [rbp+6Dh]
  unsigned __int8 v76; // [rsp+EEh] [rbp+6Eh]
  unsigned __int8 v77; // [rsp+EFh] [rbp+6Fh]
  unsigned __int8 v78; // [rsp+F0h] [rbp+70h]
  unsigned __int8 v79; // [rsp+F1h] [rbp+71h]
  unsigned __int8 v80; // [rsp+F2h] [rbp+72h]
  unsigned __int8 v81; // [rsp+F3h] [rbp+73h]
  unsigned __int8 v82; // [rsp+F4h] [rbp+74h]
  unsigned __int8 v83; // [rsp+F5h] [rbp+75h]
  unsigned __int8 v84; // [rsp+F6h] [rbp+76h]
  unsigned __int8 v85; // [rsp+F7h] [rbp+77h]
  unsigned __int8 v86; // [rsp+F8h] [rbp+78h]
  unsigned __int8 v87; // [rsp+F9h] [rbp+79h]
  int Dst[43]; // [rsp+110h] [rbp+90h]
  int i; // [rsp+1BCh] [rbp+13Ch]

  _main(*(_QWORD *)&argc, argv, envp);
  memcpy(Dst, &unk_404020, 0xA8ui64);		// Dst
  printf("plz input your flag:");
  scanf("%42s", &v46);
  v4 = 34 * v49 + 12 * v46 + 53 * v47 + 6 * v48 + 58 * v50 + 36 * v51 + v52;
  v5 = 27 * v50 + 73 * v49 + 12 * v48 + 83 * v46 + 85 * v47 + 96 * v51 + 52 * v52;
  v6 = 24 * v48 + 78 * v46 + 53 * v47 + 36 * v49 + 86 * v50 + 25 * v51 + 46 * v52;
  v7 = 78 * v47 + 39 * v46 + 52 * v48 + 9 * v49 + 62 * v50 + 37 * v51 + 84 * v52;
  v8 = 48 * v50 + 14 * v48 + 23 * v46 + 6 * v47 + 74 * v49 + 12 * v51 + 83 * v52;
  v9 = 15 * v51 + 48 * v50 + 92 * v48 + 85 * v47 + 27 * v46 + 42 * v49 + 72 * v52;
  v10 = 26 * v51 + 67 * v49 + 6 * v47 + 4 * v46 + 3 * v48 + 68 * v52;
  v11 = 34 * v56 + 12 * v53 + 53 * v54 + 6 * v55 + 58 * v57 + 36 * v58 + v59;
  v12 = 27 * v57 + 73 * v56 + 12 * v55 + 83 * v53 + 85 * v54 + 96 * v58 + 52 * v59;
  v13 = 24 * v55 + 78 * v53 + 53 * v54 + 36 * v56 + 86 * v57 + 25 * v58 + 46 * v59;
  v14 = 78 * v54 + 39 * v53 + 52 * v55 + 9 * v56 + 62 * v57 + 37 * v58 + 84 * v59;
  v15 = 48 * v57 + 14 * v55 + 23 * v53 + 6 * v54 + 74 * v56 + 12 * v58 + 83 * v59;
  v16 = 15 * v58 + 48 * v57 + 92 * v55 + 85 * v54 + 27 * v53 + 42 * v56 + 72 * v59;
  v17 = 26 * v58 + 67 * v56 + 6 * v54 + 4 * v53 + 3 * v55 + 68 * v59;
  v18 = 34 * v63 + 12 * v60 + 53 * v61 + 6 * v62 + 58 * v64 + 36 * v65 + v66;
  v19 = 27 * v64 + 73 * v63 + 12 * v62 + 83 * v60 + 85 * v61 + 96 * v65 + 52 * v66;
  v20 = 24 * v62 + 78 * v60 + 53 * v61 + 36 * v63 + 86 * v64 + 25 * v65 + 46 * v66;
  v21 = 78 * v61 + 39 * v60 + 52 * v62 + 9 * v63 + 62 * v64 + 37 * v65 + 84 * v66;
  v22 = 48 * v64 + 14 * v62 + 23 * v60 + 6 * v61 + 74 * v63 + 12 * v65 + 83 * v66;
  v23 = 15 * v65 + 48 * v64 + 92 * v62 + 85 * v61 + 27 * v60 + 42 * v63 + 72 * v66;
  v24 = 26 * v65 + 67 * v63 + 6 * v61 + 4 * v60 + 3 * v62 + 68 * v66;
  v25 = 34 * v70 + 12 * v67 + 53 * v68 + 6 * v69 + 58 * v71 + 36 * v72 + v73;
  v26 = 27 * v71 + 73 * v70 + 12 * v69 + 83 * v67 + 85 * v68 + 96 * v72 + 52 * v73;
  v27 = 24 * v69 + 78 * v67 + 53 * v68 + 36 * v70 + 86 * v71 + 25 * v72 + 46 * v73;
  v28 = 78 * v68 + 39 * v67 + 52 * v69 + 9 * v70 + 62 * v71 + 37 * v72 + 84 * v73;
  v29 = 48 * v71 + 14 * v69 + 23 * v67 + 6 * v68 + 74 * v70 + 12 * v72 + 83 * v73;
  v30 = 15 * v72 + 48 * v71 + 92 * v69 + 85 * v68 + 27 * v67 + 42 * v70 + 72 * v73;
  v31 = 26 * v72 + 67 * v70 + 6 * v68 + 4 * v67 + 3 * v69 + 68 * v73;
  v32 = 34 * v77 + 12 * v74 + 53 * v75 + 6 * v76 + 58 * v78 + 36 * v79 + v80;
  v33 = 27 * v78 + 73 * v77 + 12 * v76 + 83 * v74 + 85 * v75 + 96 * v79 + 52 * v80;
  v34 = 24 * v76 + 78 * v74 + 53 * v75 + 36 * v77 + 86 * v78 + 25 * v79 + 46 * v80;
  v35 = 78 * v75 + 39 * v74 + 52 * v76 + 9 * v77 + 62 * v78 + 37 * v79 + 84 * v80;
  v36 = 48 * v78 + 14 * v76 + 23 * v74 + 6 * v75 + 74 * v77 + 12 * v79 + 83 * v80;
  v37 = 15 * v79 + 48 * v78 + 92 * v76 + 85 * v75 + 27 * v74 + 42 * v77 + 72 * v80;
  v38 = 26 * v79 + 67 * v77 + 6 * v75 + 4 * v74 + 3 * v76 + 68 * v80;
  v39 = 34 * v84 + 12 * v81 + 53 * v82 + 6 * v83 + 58 * v85 + 36 * v86 + v87;
  v40 = 27 * v85 + 73 * v84 + 12 * v83 + 83 * v81 + 85 * v82 + 96 * v86 + 52 * v87;
  v41 = 24 * v83 + 78 * v81 + 53 * v82 + 36 * v84 + 86 * v85 + 25 * v86 + 46 * v87;
  v42 = 78 * v82 + 39 * v81 + 52 * v83 + 9 * v84 + 62 * v85 + 37 * v86 + 84 * v87;
  v43 = 48 * v85 + 14 * v83 + 23 * v81 + 6 * v82 + 74 * v84 + 12 * v86 + 83 * v87;
  v44 = 15 * v86 + 48 * v85 + 92 * v83 + 85 * v82 + 27 * v81 + 42 * v84 + 72 * v87;
  v45 = 26 * v86 + 67 * v84 + 6 * v82 + 4 * v81 + 3 * v83 + 68 * v87;
  for ( i = 0; i <= 41; ++i )
  {
    if ( *(&v4 + i) != Dst[i] )			// 关键点
    {
      printf("error");
      exit(0);
    }
  }
  printf("win");
  return 0;
}

查看unk_404020

image-20200901230739506

注意此处是小端存储

总的说来就是解那一大块线性方程组，用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
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
c = "17 4F 00 00 F6 9C 00 00 DB 8D 00 00 A6 8E 00 00 29 69 00 00 11 99 00 00 A2 40 00 00 3E 2F 00 00 B6 62 00 00 82 4B 00 00 6C 48 00 00 02 40 00 00 D7 52 00 00 EF 2D 00 00 DC 28 00 00 0D 64 00 00 8F 52 00 00 3B 61 00 00 81 47 00 00 17 6B 00 00 37 32 00 00 93 2A 00 00 5F 61 00 00 BE 50 00 00 8E 59 00 00 56 46 00 00 31 5B 00 00 3A 31 00 00 10 30 00 00 FE 67 00 00 5F 4D 00 00 DB 58 00 00 99 37 00 00 A0 60 00 00 50 27 00 00 59 37 00 00 53 89 00 00 22 71 00 00 F9 81 00 00 24 55 00 00 71 89 00 00 1D 3A 00 00".split()
ciper = []
for i in range(168//4):
    ciper.append(c[i*4+3])
    ciper[i] += c[i*4+2]
    ciper[i] += c[i*4+1]
    ciper[i] += c[i*4]
ciper = [eval(i.replace("0000","0x")) for i in ciper]
print(ciper)

from z3 import *
flag = [Int("flag%d" % i) for i in range(42)]
solver = Solver()

solver.add(ciper[4 -4]==34 * flag[3]
     + 12 * flag[0]
     + 53 * flag[1]
     + 6 * flag[2]
     + 58 * flag[4]
     + 36 * flag[5]
     + flag[6])
solver.add(ciper[5 -4]==27 * flag[4]
     + 73 * flag[3]
     + 12 * flag[2]
     + 83 * flag[0]
     + 85 * flag[1]
     + 96 * flag[5]
     + 52 * flag[6])
solver.add(ciper[6 -4]==24 * flag[2]
     + 78 * flag[0]
     + 53 * flag[1]
     + 36 * flag[3]
     + 86 * flag[4]
     + 25 * flag[5]
     + 46 * flag[6])
solver.add(ciper[7 -4]==78 * flag[1]
     + 39 * flag[0]
     + 52 * flag[2]
     + 9 * flag[3]
     + 62 * flag[4]
     + 37 * flag[5]
     + 84 * flag[6])
solver.add(ciper[8 -4]==48 * flag[4]
     + 14 * flag[2]
     + 23 * flag[0]
     + 6 * flag[1]
     + 74 * flag[3]
     + 12 * flag[5]
     + 83 * flag[6])

......（以下省略n个方程）

print(solver.check())
if solver.check() == sat:
    model = solver.model()
    result = [ chr( model[flag[i]].as_long() ) for i in range(42) ]
    print("".join(result))
    
# 来自 http://www.qfrost.com/CTF/Ciscn_2020/

正则匹配：

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
import numpy as np
from numpy.linalg import solve
dst = [0x17, 0x4F, 0x00, 0x00, 0xF6, 0x9C, 0x00, 0x00,
# 省略
0x71, 0x89, 0x00, 0x00, 0x1D, 0x3A, 0x00, 0x00]
eqs = """
v4 = 34 * v49 + 12 * v46 + 53 * v47 + 6 * v48 + 58 * v50 + 36 * v51 + v52
# 省略
v45 = 26 * v86 + 67 * v84 + 6 * v82 + 4 * v81 + 3 * v83 + 68 * v87
""".strip().split('\n')

code = []

for i in range(len(dst) // 4):
    res = 0
    t = dst[i * 4: i * 4 + 4]
    t.reverse()
    for val in t:
        res <<= 8
        res |= val
    code.append(res)
print(len(code))
print(list(map(hex, code)))

import re
patt = r'\+?\s*(?P<coeff>\d*)?\s*\*?\s*v(?P<x>\d*)'
rgx = re.compile(patt)
coeffs = []
for eq in eqs:
    eq_parts = [m.groupdict() for m in rgx.finditer(eq)][1:]
    coeff = [0 for _ in range(42)]
    print(eq)
    for eqp in eq_parts:
    # print(eqp)
        c = int(eqp['coeff']) if eqp['coeff'] != '' else 1
        x = int(eqp['x'])
        coeff[x - 46] = c
    print(coeff)
    coeffs.append(coeff)
    
import numpy as np
from numpy.linalg import solve
a = np.mat(coeffs)
b = np.array(code)
x = solve(a, b)
for c in x:
print(chr(int(round(c))), end='')

hyperthreading

放进 IDA 里反编译查看一下，发现与 z3 类似是将输入进行变换后比较。大致查看变换 过程，可见是以一个字符为变换单元。 使用 ollydbg 进行动态调试，输入数字和小写字母。在最后的比较处下断点，然后在查 看内存中相应的数据，可以得到输入的数字、字母和输出的数据的对应关系，以及目 标数据。图中最上面是目标数据，第二部分是数字 0-9 对应的输出，第三部分是小写 字母 a-z 对应的输出，最后是大写字母（题目中未出现）。代入目标数据得到大部分 结果，猜测 20 和 9F 分别对应{和}，在输入特殊字符尝试，得到 8B 对应的输入应该是 -。

脚本：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
ciper = [
    0xDD, 0x5B, 0x9E, 0x1D, 0x20, 0x9E, 0x90, 0x91, 0x90, 0x90, 
    0x91, 0x92, 0xDE, 0x8B, 0x11, 0xD1, 0x1E, 0x9E, 0x8B, 0x51, 
    0x11, 0x50, 0x51, 0x8B, 0x9E, 0x5D, 0x5D, 0x11, 0x8B, 0x90, 
    0x12, 0x91, 0x50, 0x12, 0xD2, 0x91, 0x92, 0x1E, 0x9E, 0x90, 
    0xD2, 0x9F
]

for i in range(len(ciper)):
    ciper[i] -= 0x23
    if ciper[i] <0:
        ciper[i] += 0x100
    ciper[i] ^= 0x23
    ciper[i] = ((ciper[i] >> 6) ^ (ciper[i]<<2))&0xFF
print(ciper)
print("".join([chr(i) for i in ciper]))

# 来自 http://www.qfrost.com/CTF/Ciscn_2020/