CTF-Reverse学习记录

 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

char base64_table[] = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"
int __fastcall base64_encode(char *Str2, char *Str)
{
  int v3; // [rsp+24h] [rbp-1Ch]
  int v4; // [rsp+34h] [rbp-Ch]
  int v5; // [rsp+38h] [rbp-8h]
  int v6; // [rsp+3Ch] [rbp-4h]

  v3 = strlen(Str);
  if ( v3 % 3 )
    v6 = 4 * (v3 / 3 + 1);
  else
    v6 = 4 * (v3 / 3);
  Str2[v6] = 0;
  v5 = 0;
  v4 = 0;
  while ( v6 - 2 > v5 )
  {
    Str2[v5] = base64_table[(unsigned __int8)Str[v4] >> 2]; // 右移2位，获得第一个字符前6位的数据
    Str2[v5 + 1] = base64_table[(16 * (Str[v4] & 3)) | ((unsigned __int8)Str[v4 + 1] >> 4)]; // 获取第二个6位
    Str2[v5 + 2] = base64_table[(4 * (Str[v4 + 1] & 0xF)) | ((unsigned __int8)Str[v4 + 2] >> 6)]; // 获得第三个6位
    Str2[v5 + 3] = base64_table[Str[v4 + 2] & 0x3F]; // 获得第四个6位
    v4 += 3;
    v5 += 4;
  }
  if ( v3 % 3 == 1 )
  {
    Str2[v5 - 2] = "=";
    Str2[v5 - 1] = "=";
  }
  else if ( v3 % 3 == 2 )
  {
    Str2[v5 - 1] = "=";
  }
  return putchar("\n");
}

1
2
3
4
5

__asm {
    _emit 0xE8
    _emit 0xFF
   //_emit 立即数：代表在这个位置插入一个数据，这里插入的是0xe8
}

1
2
3
4
5

 __asm {
        jz Label;
		jnz Label;
		_emit 0xC7;
Label:

1
2
3
4

# 下载
upx: https://github.com/upx/upx
# 使用方法
upx -d re.exe

1
2
3

# 可以用如下命令进行解包
[+] Usage: pyinstxtractor.py <filename>
# 这里要注意，如果本地版本和出题人打包用的版本不同，某些依赖可能无法正常解包

1
2
3

https://tool.lu/pyc/
https://www.lddgo.net/string/pyc-compile-decompile
https://www.toolkk.com/tools/pyc-decomplie

1
2
3
4
5
6

# 直接 pip 安装即可
pip3 install uncompyle6
# 然后将 Script 目录添加到环境变量中
C:\Users\XXX\AppData\Local\Programs\Python\Python38\Scripts
# 之后就可以直接在终端中使用了
uncompyle6 filename.pyc > decompile.py

1

python pyinstxtractor.py reverse_1_PyHaHa.pyc

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14

# 下载并编译
git clone https://github.com/zrax/pycdc.git
mkdir build && cd build
cmake ..
make -j$(nproc)

# 使用方法
Usage:  ./pycdc [options] input.pyc

Options:
  -o <filename>  Write output to <filename> (default: stdout)
  -c             Specify loading a compiled code object. Requires the version to be set
  -v <x.y>       Specify a Python version for loading a compiled code object
  --help         Show this help text and then exit

 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

from z3 import *

# 1. 创建变量
x = Int('x')      # 整型变量
y = Int('y')      # 整型变量
p = Bool('p')     # 布尔变量p
q = Bool('q')     # 布尔变量q
r = Bool('r')     # 布尔变量r

# 2. 创建求解器
s = Solver()

# 3. 添加约束条件
# 数值约束
s.add(x > 0)                    # x必须大于0
s.add(y > 0)                    # y必须大于0
s.add(x + y == 10)              # x+y等于10
s.add(Implies(p, x > y))        # 如果p为真，则x>y

# 逻辑约束
s.add(Implies(p, q))            # p → q (如果p为真，则q为真)
s.add(r == Not(q))              # r = ¬q (r等于q的否定)
s.add(Or(Not(p), r))            # ¬p ∨ r (p的否定或r为真)

# 4. 检查约束是否可满足
if s.check() == sat:
    # 5. 获取解
    m = s.model()
    print(f"找到解：x = {m[x]}, y = {m[y]}")
    print(f"逻辑变量：p = {m[p]}, q = {m[q]}, r = {m[r]}")
else:
    print("约束不可满足")

 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

from z3 import *

enc = [0x0000B1B0, 0x00005678, 0x00007FF2, 0x0000A332, 0x0000A0E8, 0x0000364C, 0x00002BD4, 0x0000C8FE, 0x00004A7C, 0x00000018, 0x00002BE4, 0x00004144, 0x00003BA6, 0x0000BE8C, 0x00008F7E, 0x000035F8, 0x000061AA, 0x00002B4A, 0x00006828, 0x0000B39E, 0x0000B542, 0x000033EC, 0x0000C7D8, 0x0000448C, 0x00009310, 0x00008808, 0x0000ADD4, 0x00003CC2, 0x00000796, 0x0000C940, 0x00004E32, 0x00004E2E, 0x0000924A, 0x00005B5C]

s = Solver()

input = [BitVec(f"input{i}", 8) for i in range(34)] # input0-input33 都是 0-255
var = [BitVec(f"var{i}",32) for i in range(34)] # var0-var31 都是 0-4294967295

# 模拟加密算法
for i in range(34):
    var[i] = 47806 * (ZeroExt(24, input[i]) + i) # 高位补零，将8位扩展至32位
    if i:
        var[i] ^= var[i-1] ^ 0x114514
    var[i] %= 51966

# 添加约束条件
for i in range(34):
    s.add(var[i] == enc[i])

while True:
    if s.check() == sat: # 找到解
        m = s.model()
        ascii_list = [m[input[i]].as_long() for i in range(34)] # 将Z3的符号值转换为Python的普通整数
        flag = "moectf{"  + "".join(chr(ascii_list[i]) for i in range(34)) + "}"
        print(flag)

        # 添加阻塞条件，寻找下一个解
        block = []
        for i in range(34):
            block.append(input[i] != m[input[i]])
        s.add(Or(block)) # 至少有一个变量与当前解不同
    else:
        break