Post

ehaxCTF - ghostKey

Posted
By 9vvert
18 min read
ehaxCTF - ghostKey

0x01 编写gdb脚本辅助ai分析

程序要求输入一个32字节的key, 直接让ai静态分析，但是效果不好. 让ai生成需要dump的断点：

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

   ## 1) charset 检查（main.main.func2）

  ### 断点A：0x499a4c（取当前字符）

  - IDA语义：r = k[i]（对应伪代码里的 r）
  - 观察变量：
      - i -> rcx
      - key_len -> rbx
      - key_ptr -> rax
      - 当前字符 -> byte ptr [rax+rcx]

  GDB：

  b *0x499a4c
  commands
    silent
    printf "i=%llu len=%llu\n", $rcx, $rbx
    x/1bx $rax+$rcx
    c
  end

  ### 断点B：0x499a80（范围判断前一拍）

  - IDA语义：刚做完 r-0x20，下一条就是 cmp edx,0x5e
  - 观察变量：
      - edx 此时是 r-0x20
      - 原字符可看 edx+0x20

  GDB：

  b *0x499a80
  commands
    silent
    printf "r_minus_20=0x%x, r=0x%x\n", $edx, (($edx+0x20)&0xffffffff)
    c
  end

  ———

  ## 2) aesCheck（main.aesCheck）

  ### 断点C：0x498ec9（SHA256 结果已写入 key[32]）

  - IDA变量：key（栈上，偏移 rsp+0x38）
  - 观察：
      - SHA256(k[:16]) 的 32 字节

  GDB：

  b *0x498ec9
  commands
    silent
    x/32bx $rsp+0x38
    c
  end

  ### 断点D：0x498f31（MD5 结果写入 IV 缓冲）

  - IDA变量：
      - var_10（rsp+0xa8）里存的是 IV 指针
      - *var_10 是 16 字节 IV
  - 观察：
      - MD5(k[16:])

  GDB：

  b *0x498f31
  commands
    silent
    set $ivp = *(unsigned long*)($rsp+0xa8)
    x/16bx $ivp
    c
  end

  ———

  ## 3) CBC 解密调用点（你点名的 0x498fc9）

  ### 断点E：0x498fc9（call 前）

  - IDA变量：
      - ptr 在 rsp+0xa0（明文输出缓冲指针）
      - 密文是全局 main_encryptedFlag（地址 0x58e560）
  - 观察：
      - 调用前确认 ptr 地址、密文内容

  GDB：

  b *0x498fc9
  commands
    silent
    set $pt = *(unsigned long*)($rsp+0xa0)
    printf "pt=%p\n", $pt
    x/32bx 0x58e560
    c
  end

  ### 断点F：0x498fcb（call 后，最关键）

  - 观察：
      - ptr 指向的 32 字节解密结果
      - 是否以 crackme{ 开头

  GDB：

  b *0x498fcb
  commands
    silent
    set $pt = *(unsigned long*)($rsp+0xa0)
    x/32bx $pt
    x/s $pt
    c
  end

让codex写了一个脚本模板然后手改~

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
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183

# hook_dump.py
# 在 GDB 里：source hook_dump.py
# 例：gdb -q -x hook_dump.py --args ./a.out

import gdb
import os
import time
import argparse
import struct

commandline = 'A' * 32
if os.path.exists("flag.txt"):
    try:
        commandline = open("flag.txt", "r", encoding="utf-8").read().strip() or commandline
    except Exception:
        pass

# NOTE: handler对象：self(Breakpoint对象)， frame, addr
def handler_default(bp, frame, hit_addr: int):
    gdb.write(f"[default] hit @ {hit_addr:#x}\n")

def handler_len(bp, frame, hit_addr: int):
    print(f'in handler_len, addr:{hex(hit_addr)}')
    gdb.execute("x/gx $rdx+0x10")
    # gdb.execute("c")

def handler_lfsr(bp, frame, hit_addr: int):
    print(f'in handler_lfsr, addr:{hex(hit_addr)}')
    print('print v4:')
    gdb.execute("p/x $bx")
    # gdb.execute("c")

def handler_nible(bp, frame, hit_addr: int):
    print(f'in handler_nible, addr:{hex(hit_addr)}')
    print('print v10:')
    gdb.execute("x/wx $rsp+0x10")
    # gdb.execute("c")

def handler_column(bp, frame, hit_addr: int):
    print(f'in handler_column, addr:{hex(hit_addr)}')
    print('print v7 % 0x61:')
    gdb.execute("p/x $sil")
    # gdb.execute("c")

def handler_pairs(bp, frame, hit_addr: int):
    print(f'in handler_pairs, addr:{hex(hit_addr)}')
    print('print (v1[a]+v1[b])%mod:')
    gdb.execute("p/x $dl")
    # gdb.execute("c")

def handler_sbox(bp, frame, hit_addr: int):
    print(f'in handler_sbox, addr:{hex(hit_addr)}')
    print('print v4:')
    gdb.execute("p/x $dl")
    # gdb.execute("c")

def handler_tagCheck(bp, frame, hit_addr: int):
    print(f'in handler_tagCheck, addr:{hex(hit_addr)}')
    print('print k[4i]^k[4i+1]^k[4i+2]^k[4i+3]:')
    gdb.execute("p/x $dil")
    # gdb.execute("c")

def handler_charset(bp, frame, hit_addr: int):
    print(f'in handler_charset, addr:{hex(hit_addr)}')
    print('print k[i]:')
    gdb.execute("x/1bx $rax+$rcx")
    # gdb.execute("c")

def handler_aesCheck(bp, frame, hit_addr: int):
    print(f'in handler_aesCheck, addr:{hex(hit_addr)}')
    print('print SHA256(k[:16]):')
    gdb.execute("x/32bx $rsp+0x38")
    # gdb.execute("c")

def handler_md5(bp, frame, hit_addr: int):
    print(f'in handler_md5, addr:{hex(hit_addr)}')
    print('print MD5(k[16:]:')
    inf = gdb.selected_inferior()
    rsp = int(gdb.parse_and_eval("$rsp"))
    ivp = struct.unpack("<Q", bytes(inf.read_memory(rsp + 0xA8, 8)))[0]
    gdb.write(f"ivp={ivp:#x}\n")
    gdb.execute(f"x/16bx {ivp:#x}")
    # gdb.execute("c")

def handler_cbc(bp, frame, hit_addr: int):
    print(f'in handler_cbc, addr:{hex(hit_addr)}')
    print('print info:')
    inf = gdb.selected_inferior()
    rsp = int(gdb.parse_and_eval("$rsp"))
    pt = struct.unpack("<Q", bytes(inf.read_memory(rsp + 0xA0, 8)))[0]
    gdb.write(f"pt={pt:#x}\n")
    gdb.execute("x/32bx 0x58e560")
    # gdb.execute("c")

def handler_decrypt(bp, frame, hit_addr: int):
    print(f'in handler_decrypt, addr:{hex(hit_addr)}')
    print('print info:')
    inf = gdb.selected_inferior()
    rsp = int(gdb.parse_and_eval("$rsp"))
    pt = struct.unpack("<Q", bytes(inf.read_memory(rsp + 0xA0, 8)))[0]
    gdb.execute(f'x/32bx {pt:#x}')
    gdb.execute(f'x/s {pt:#x}')
    gdb.write(f"pt={pt:#x}\n")
    gdb.execute("x/32bx 0x58e560")
    # gdb.execute("c")

def handler_check_fail_bypass(bp, frame, hit_addr: int):
    print(f'in handler_check_fail_bypass, addr:{hex(hit_addr)}')
    print('bypass failed sub-check -> continue next check item')
    gdb.execute("set $rip = 0x4994c5")

# TODO: 添加地址 -> handler函数映射
ADDR_DISPATCH = {
    # 这里填你想根据“命中地址”区分的点
    0x499aa0: handler_len,
    0x4999E2: handler_lfsr,
    0x499973: handler_nible,
    0x4998CF: handler_column,
    0x499854: handler_pairs,
    0x4997C7: handler_sbox,
    0x498D73: handler_tagCheck,
    0x499a4c: handler_charset,
    0x498f34: handler_aesCheck,
    0x498f31: handler_md5,
    0x498fc9: handler_cbc,
    0x498fcb: handler_decrypt,
    0x49951b: handler_check_fail_bypass,

}

def dispatch(hit_addr: int):
    if hit_addr in ADDR_DISPATCH:
        return ADDR_DISPATCH[hit_addr]
    return handler_default

# ---------- 自定义断点类 ----------
class RoutedBreakpoint(gdb.Breakpoint):
    def __init__(self, spec: str, internal=False):
        super().__init__(spec, internal=internal)
        self.silent = True  # 不让 gdb 自己打印“Breakpoint N, ...”
        gdb.write(f"[+] Breakpoint set: {spec} (num={self.number})\n")

    def stop(self):
        # 命中时拿 PC/RIP
        frame = gdb.selected_frame()
        arch = frame.architecture().name()
        # gdb 里 $pc 通常可用；x86_64 下也可以用 $rip
        # TIP: gdb的parse_and_eval函数可以解析表达式；然后就是类型转换
        try:
            hit_addr = int(gdb.parse_and_eval("$pc"))
        except gdb.error:
            hit_addr = int(gdb.parse_and_eval("$rip"))

        # 如果你更想用“断点本身的地址”（而不是当前 pc），也可以：
        # hit_addr = int(self.location, 0)  # 但 location 可能是 symbol/表达式，不总能转
        handler = dispatch(hit_addr)

        gdb.write(f"[*] stop: bp#{self.number} pc={hit_addr:#x} arch={arch}\n")
        handler(self, frame, hit_addr)

        # NOTE:
        # True：停下来给你交互；False：执行完自动 continue
        # 如果你想“自动 dump 然后继续跑”，就 return False
        return False

# ---------- 初始化：你要的断点 ----------
def main():
    # 示例：对符号/地址/表达式下断点都可以
    # RoutedBreakpoint("*0x401234")
    # RoutedBreakpoint("malloc")
    # RoutedBreakpoint("read")
    #
    # 你也可以下条件断点：breakpoint 的 spec 写成 "*(0x...)" 后再 bp.condition = "..."
    # b = RoutedBreakpoint("*0x401234"); b.condition = "$rdi == 0xdeadbeef"
    # 这里先给出两个演示断点（按你程序改）
    # RoutedBreakpoint("main")

    for addr in sorted(ADDR_DISPATCH.keys()):
        RoutedBreakpoint(f"*{addr:#x}")   # 例如 "*0x498fc9"

    gdb.write("[+] hook_dump.py loaded.\n")
    gdb.execute(f'r {commandline}')
main()
  • gdb.execute可以执行命令；
  • gdb.parse_and_eval可以获得寄存器/变量的值
  • 继承gdb.Breakpoint类，重写其中的init和stop函数可以实现hook的行为. stop中通过dispatch函数判断断点是否位于特定地址（实现了根据不同位置，执行不同的dump逻辑）
  • 为了让断点dump后能继续运行，在stop函数中return False。不要在handler函数中增加gdb.execute("c"). 刚开始我stop函数中return True, 然后使用类似：
    1
2
3
4

    def handler_len(bp, frame, hit_addr: int):
  print(f'in handler_len, addr:{hex(hit_addr)}')
  gdb.execute("x/gx $rdx+0x10")
  gdb.execute("c")

    的函数来尝试继续运行，但是在运行时报错：

    1

    in handler_len, addr:0x499aa0 0xc00000e028: 0x0000000000000020 Python Exception <class 'gdb.error'>: Cannot execute this command while the selected thread is running.

    GPT分析： 这是因为你在 Python 断点回调（stop()/handler）里调用了 gdb.execute("c")。
    当你在断点回调里执行 continue（c）时，GDB 会让线程继续运行；但你的 Python 代码还没返回，GDB 仍在“处理停止事件”的上下文里. 正确做法（推荐）：不要在 handler 里 c，而是让 stop() 返回 False 自动继续

0x02 语义分析

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

• 输入开始到输出的完整流程如下：

  1. 读取输入

  - 程序要求参数个数为 2：./ghost <32-char key>
  - 不满足则打印 Usage: %s <32-char key> 并退出。

  2. 8 个前置校验（按顺序）

  - length：长度必须是 32。
  - charset：每个字符必须在 0x20..0x7e（可打印 ASCII）。
  - lfsr：以初始状态 0xACE1 对 32 字节逐 bit 更新，最终状态必须等于 targetLFSR(0x4358)。
  - nibble：把 32 字节分成 4 组，每组 8 字节；每字节算 (high_nibble ^ low_nibble)，组内再异或，结果要等于 targetNibble 4 字节。
  - colsum：按 4x8 矩阵看 key（索引 i,i+8,i+16,i+24 为一列），每列和 %97 要等于 targetColSums[8]。
  - pairs：12 组 (a,b,mod,res)，要求 (key[a]+key[b]) % mod == res。
  - sbox：取偶数位字节 key[0],key[2],... 过 AES S-box 后累积异或，结果必须是 0x66。
  - tag：每 4 字节一组，k[4i]^k[4i+1]^k[4i+2]^k[4i+3] == targetTag[i]（8 组）。

  任一失败：打印

  - [-] Check failed: <name>
  - Wrong key. Keep reversing.
    然后退出。

  3. 进入 aesCheck（前置都通过后）

  - 把 key 转字节切片。
  - aes_key = SHA256(key[:16])（前 16 字节）。
  - iv = MD5(key[16:])（后 16 字节）。
  - 用 AES-CBC 解密内置 32 字节密文 encryptedFlag。
  - 检查解密明文前 8 字节是否等于 flagPrefix = "crackme{"。
      - 不等：aesCheck 返回 false。
      - 相等：返回 true + 32 字节明文字符串。

  4. 最终输出

  - aesCheck 失败：
      - [-] Check failed: aes_verify
      - Wrong key. Keep reversing.
  - 成功：
      - All checks passed!
      - [+] Flag: %s（即解密出的明文）

  核心关系一句话：
  输入 32 字符 key -> 通过 8 层约束 -> 派生 SHA256/MD5 -> AES-CBC 解密 -> 前缀验证 -> 输出 flag。

0x03 编写z3脚本

让codex自己编写脚本时，它总是将所有的约束都加进去，跑了一晚上都没有跑出来。

晚上躺在床上的时候，我开始想：能否调整约束的顺序，比如加入其中某些条件约束比较强，能够直接推断出某些字符，会不会减少一些工作量？（当晚睡前还没有听睡眠歌单，直接失眠了~）

第二天醒来又看了看发现最后一步的限制crackme{还需要依赖hash + AES-decrypt，不可逆，所以只能放在最后验证。

但是顺着这个思路我突然想到：里面有一些非线性的计算，比如sbox-mapping，这对z3求解会带来很多的工作量，如果把这个部分放到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
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
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190

#!/usr/bin/env python3
# -*- coding: utf-8 -*-

import argparse

from z3 import *

TARGET_LFSR = 0x4358
INIT_LFSR = 0xACE1
POLY = 0xB400

TARGET_NIBBLE = [0x08, 0x08, 0x04, 0x07]
TARGET_COLSUM = [12, 39, 8, 0, 55, 33, 50, 96]
TARGET_TAG = [108, 117, 58, 1, 126, 47, 52, 0]

PAIRS = [
    (0, 31, 0x7F, 0x68),
    (3, 28, 0x83, 0x11),
    (7, 24, 0x71, 0x35),
    (11, 20, 0x6D, 0x3A),
    (1, 15, 0x67, 0x34),
    (5, 27, 0x61, 0x58),
    (9, 22, 0x6B, 0x14),
    (13, 18, 0x65, 0x40),
    (2, 29, 0x7F, 0x51),
    (6, 25, 0x83, 0x76),
    (10, 21, 0x71, 0x28),
    (14, 17, 0x6D, 0x53),
]

# AES S-box used by check7
SBOX = bytes.fromhex(
    "637c777bf26b6fc53001672bfed7ab76"
    "ca82c97dfa5947f0add4a2af9ca472c0"
    "b7fd9326363ff7cc34a5e5f171d83115"
    "04c723c31896059a071280e2eb27b275"
    "09832c1a1b6e5aa0523bd6b329e32f84"
    "53d100ed20fcb15b6acbbe394a4c58cf"
    "d0efaafb434d338545f9027f503c9fa8"
    "51a3408f929d38f5bcb6da2110fff3d2"
    "cd0c13ec5f974417c4a77e3d645d1973"
    "60814fdc222a908846eeb814de5e0bdb"
    "e0323a0a4906245cc2d3ac629195e479"
    "e7c8376d8dd54ea96c56f4ea657aae08"
    "ba78252e1ca6b4c6e8dd741f4bbd8b8a"
    "703eb5664803f60e613557b986c11d9e"
    "e1f8981169d98e949b1e87e9ce5528df"
    "8ca1890dbfe6426841992d0fb054bb16"
)


def build_solver_all_constraints(enable_sbox: bool):
    s = Solver()
    # You can tune this locally as needed.
    s.set(timeout=0)

    b = [BitVec(f"b{i:02d}", 8) for i in range(32)]

    # printable ASCII
    for x in b:
        s.add(UGE(x, 0x20), ULE(x, 0x7E))

    # check8: tag (every 4 bytes xor)
    for i in range(8):
        a = 4 * i
        t = b[a] ^ b[a + 1] ^ b[a + 2] ^ b[a + 3]
        s.add(t == BitVecVal(TARGET_TAG[i], 8))

    # check4: nibble groups (4 groups * 8 bytes)
    for g in range(4):
        x = BitVecVal(0, 8)
        base = 8 * g
        for j in range(8):
            v = b[base + j]
            x = x ^ (LShR(v, 4) ^ (v & BitVecVal(0x0F, 8)))
        s.add(x == BitVecVal(TARGET_NIBBLE[g], 8))

    # check5: column sums mod 97
    for i in range(8):
        col_sum = (
            ZeroExt(8, b[i])
            + ZeroExt(8, b[i + 8])
            + ZeroExt(8, b[i + 16])
            + ZeroExt(8, b[i + 24])
        )
        s.add(URem(col_sum, BitVecVal(97, 16)) == BitVecVal(TARGET_COLSUM[i], 16))

    # check6: pair constraints
    for a, c, modv, rv in PAIRS:
        pair_sum = ZeroExt(8, b[a]) + ZeroExt(8, b[c])
        s.add(URem(pair_sum, BitVecVal(modv, 16)) == BitVecVal(rv, 16))

    # check7: optional sbox xor for even indices
    if enable_sbox:
        sbox_arr = K(BitVecSort(8), BitVecVal(0, 8))
        for i, v in enumerate(SBOX):
            sbox_arr = Store(sbox_arr, BitVecVal(i, 8), BitVecVal(v, 8))

        sx = BitVecVal(0, 8)
        for i in range(0, 32, 2):
            sx = sx ^ Select(sbox_arr, b[i])
        s.add(sx == BitVecVal(0x66, 8))

    # check3: lfsr rolling over all 32 bytes, branch-free bit-vector form
    state = BitVecVal(INIT_LFSR, 16)
    poly = BitVecVal(POLY, 16)

    for i in range(32):
        for k in range(8):
            u = ZeroExt(15, Extract(k, k, b[i]))
            lsb = (state ^ u) & BitVecVal(1, 16)
            mask = -lsb  # 0x0000 if lsb=0, 0xFFFF if lsb=1
            state = LShR(state, 1) ^ (poly & mask)

    s.add(state == BitVecVal(TARGET_LFSR, 16))

    return s, b


def sbox_check_py(out: bytes) -> bool:
    x = 0
    for i in range(0, 32, 2):
        x ^= SBOX[out[i]]
    return x == 0x66


def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--sbox", type=str, default="false")
    ap.add_argument("--all", type=str, default="false")
    ap.add_argument("--max-solutions", type=int, default=20)
    ap.add_argument("--threads", type=int, default=1)
    args = ap.parse_args()

    enable_sbox = str(args.sbox).lower() == "true"
    enumerate_all = str(args.all).lower() == "true"
    solver, bytes_ = build_solver_all_constraints(enable_sbox=enable_sbox)
    solver.set(threads=max(1, args.threads))

    print(
        f"[*] Solving all non-AES constraints... "
        f"(sbox_in_solver={enable_sbox}, all={enumerate_all}, threads={max(1, args.threads)})"
    )
    if not enable_sbox:
        print("[*] S-box will be checked outside Z3 on enumerated solutions.")

    if not enumerate_all:
        r = solver.check()
        print("[*] solver result:", r)
        if r != sat:
            return
        m = solver.model()
        out = bytes([m.evaluate(x, model_completion=True).as_long() & 0xFF for x in bytes_])
        print("[+] candidate key (hex):", out.hex())
        print("[+] candidate key (ascii):", out.decode("ascii", errors="replace"))
        if not enable_sbox:
            print(f"[+] sbox_check_py={sbox_check_py(out)}")
        return

    found = 0
    sbox_pass = 0
    while found < max(1, args.max_solutions):
        r = solver.check()
        if r != sat:
            print(f"[*] enumeration finished: {r}, total={found}, sbox_pass={sbox_pass}")
            break

        m = solver.model()
        out = bytes([m.evaluate(x, model_completion=True).as_long() & 0xFF for x in bytes_])
        found += 1
        if enable_sbox:
            print(f"[+] solution #{found} hex: {out.hex()}")
            print(f"[+] solution #{found} ascii: {out.decode('ascii', errors='replace')}")
        else:
            ok = sbox_check_py(out)
            if ok:
                sbox_pass += 1
            print(f"[+] solution #{found} sbox_ok={ok} hex: {out.hex()}")
            if ok:
                print(f"[+] solution #{found} ascii: {out.decode('ascii', errors='replace')}")

        # Block current model and continue.
        solver.add(Or([x != m.evaluate(x, model_completion=True) for x in bytes_]))

    if found >= max(1, args.max_solutions):
        print(f"[*] hit max-solutions={args.max_solutions}, stop. sbox_pass={sbox_pass}")


if __name__ == "__main__":
    main()

运行：

1

python3 -u solve.py --all=true --threads=4

跑了大概20分钟就跑出了key: 解密得到flag:

1

crackme{AES_gh0stk3y_r3v3rs3d!!}
ctf2026, ehaxCTF
rev z3
This post is licensed under CC BY 4.0 by the author.