NOP

IDA中执行以下python脚本

1
2
3
4
5
6
7
8
import ida_bytes

# 替换指定地址范围内的指令为 NOP
start_addr = 0x401000 # 起始地址
end_addr = 0x401010 # 结束地址

for addr in range(start_addr, end_addr):
    ida_bytes.patch_byte(addr, 0x90) # 0x90 是 NOP 指令的机器码

z3

题目

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
__int64 __fastcall check(__int64 a1)
{
  int i; // [rsp+1Ch] [rbp-4h]

  for ( i = 0; i <= 33; ++i )
  {
    check(std::string)::b[i] = 47806 * (*(char *)std::string::operator[](a1, i) + i);
    if ( i )
      check(std::string)::b[i] ^= check(std::string)::b[i - 1] ^ 0x114514;
    check(std::string)::b[i] %= 51966;
    if ( check(std::string)::b[i] != a[i] )
      return 0;
  }
  return 1;
}
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
# pip install z3-solver
from z3 import *

# ----- a[0..33] 常量表 -----
a = [
    0x0B1B0, 0x5678, 0x7FF2, 0x0A332, 0x0A0E8, 0x364C, 0x2BD4,
    0x0C8FE, 0x4A7C, 0x18,    0x2BE4, 0x4144, 0x3BA6, 0x0BE8C, 0x8F7E,
    0x35F8, 0x61AA, 0x2B4A, 0x6828,  0x0B39E, 0x0B542, 0x33EC, 0x0C7D8,
    0x448C, 0x9310, 0x8808,  0x0ADD4, 0x3CC2, 0x796,   0x0C940, 0x4E32,
    0x4E2E, 0x924A, 0x5B5C,
]
assert len(a) == 34

# ----- 可调参数 -----
PRINTABLE_ASCII_ONLY = True  # True: 只允许 32..126 可打印字符；False: 放开为 0..255
MAX_SOLUTIONS = 10           # 枚举前 N 个不同解

def build_solver():
    N = 34
    s = [BitVec(f"s_{i}", 8) for i in range(N)]

    sol = Solver()

    # 域约束
    if PRINTABLE_ASCII_ONLY:
        for i in range(N):
            sol.add(UGE(s[i], BitVecVal(32, 8)))
            sol.add(ULE(s[i], BitVecVal(126, 8)))
    # 放开域时，BitVec(8) 自带 0..255，无需加约束

    # check 逻辑约束
    MOD   = BitVecVal(51966, 64)
    MUL   = BitVecVal(47806, 64)
    MAGIC = BitVecVal(0x114514, 64)

    for i in range(N):
        term = MUL * (ZeroExt(56, s[i]) + BitVecVal(i, 64))
        if i == 0:
            x = term
        else:
            x = term ^ (BitVecVal(a[i-1], 64) ^ MAGIC)

        rem = URem(x, MOD)                # <-- 关键：无符号取模
        sol.add(rem == BitVecVal(a[i], 64))

    return sol, s

def model_to_inner(m, s_vars):
    bs = [m[v].as_long() for v in s_vars]
    try:
        return bytes(bs).decode("latin1")
    except Exception:
        return "".join(chr(b) for b in bs)

def main():
    sol, s_vars = build_solver()
    solutions = []

    while len(solutions) < MAX_SOLUTIONS and sol.check() == sat:
        m = sol.model()
        inner = model_to_inner(m, s_vars)
        flag = f"moectf{{{inner}}}"
        solutions.append(flag)

        # 阻塞当前解：至少有一个字节不同
        sol.add(Or([s_vars[i] != m[s_vars[i]] for i in range(len(s_vars))]))

    print(f"[域] {'ASCII(32..126)' if PRINTABLE_ASCII_ONLY else 'BYTE(0..255)'}")
    print(f"[找到] {len(solutions)} 个解（最多枚举 {MAX_SOLUTIONS} 个）\n")
    for idx, f in enumerate(solutions, 1):
        print(f"[{idx}] {f} (len={len(f)})")
    if not solutions and PRINTABLE_ASCII_ONLY:
        print("\n提示：把 PRINTABLE_ASCII_ONLY=False 可放宽域，可能出现更多解。")

if __name__ == "__main__":
    main()

flower

alt text
F5失败

去找solve按住空格，得到汇编代码
alt text

找到错误的地方
alt text

可以看到jz和jnz两个跳转一定有一个会成立, 所以这个 call 是永远不会被执行的, 但是会导致IDA的调用栈识别错误
先把jz和jnz都nop掉，然后u+c+p，即可恢复正常

现在solve函数就能F5了