TL;DR

Go 1.22.2 바이너리 VM

Analysis

Default

주요 패키지: Go_Mixer/internal/vvvv, Go_Mixer/internal/oracle

prompt $\rightarrow$ must $\rightarrow$ main 흐름은 크게 다음과 같다.

prompt() 로 문자열 받기
strings.TrimSpace로 개행 정리
Go_Mixer/internal/deriv 함수 3개 호출로 VM 초기 데이터 복호화
vvvv. (*Machine). Run 으로 VM 실행
정답 테이블과 비교해 일치하면 플래그 출력

fmt.Fprintln 부분부터 추적했다.

주요 함수

Go_Mixer/internal/vvvv.(*Machine).preloadInputBERev (0x4861c0)
Go_Mixer/internal/vvvv.localMap (0x486300)
Go_Mixer/internal/vvvv.(*Machine).Run (0x486400)
Go_Mixer/internal/vvvv.adsfmdslfalf (0x486a60)
Go_Mixer/internal/vvvv.cxzcxz (0x486b20)
Go_Mixer/internal/vvvv.udsmlkf (0x486c00)
Go_Mixer/internal/vvvv.ccxvl (0x486fa0)
Go_Mixer/internal/vvvv.xuwml (0x487320)
Go_Mixer/internal/vvvv.xvcmxlvx (0x487620)
Go_Mixer/internal/vvvv.quwerw (0x4874a0)
main.must (0x487e60)

VM Machine

main.main에서 runtime_newobject(&RTYPE_vvvv_Machine, ...) 호출 이후 구조체 필드를 채우는 부분이 있다.

1
(gdb) x/4gx 0x531420
2
0x531420: 0x7233765f79723376 0x7433726333735f79
3
0x531430: 0x7230665f79336b5f 0x6861685f7530795f

preloadInputBERev 단계에서 DjNv3ry_v3ry_s3cr3t_k3y_f0r_y0u_hah이 메모리에 적재됐다.

1
(gdb) x/16gx 0x531660
2
0x531660: 0x82ce0803 0xed0a0ade 0x5eb83efd 0xdd86d41a
3
..

VM이 최종 비교에 사용하는 16개의 32비트 값.

AES-CTR

Go_Mixer/internal/deriv.xorCTR 를 보면 키 문자열을 두 덩이(16바이트 nonce + 16바이트 key)로 쪼개 crypto/aes + cipher.NewCTR를 사용한다. VM용 S-Box와 곱셈 상수를 복호화한다.

vvvv.Machine에는 다음 값이 채워진다.

machine.sbox = 키 앞 16바이트
machine.mul = 0x4E6A44B9
machine.key = 전체 32바이트
machine.mem = 길이 128짜리 uint32 배열

1
sbox 030e010a04090506080b0f020d0c0007
2
    mul 1315587257
3
    target ['0x82ce0803', '0xed0a0ade', '0x5eb83efd', '0xdd86d41a', '0xc635b860', '0x2115b7f1', '0xf57d3092', '0x17a52348', '0x223c75ae',
4
    '0xdf525a75', '0x3773e5f4', '0xfd0e81a6', '0x87f325a8', '0x5cd21a47', '0x2290027e', '0x74d1bfed']

VM Instruction

바이너리 안에는 opcode 스트림이 그대로 들어 있다. 주소 0x535DA0 부근을 덤프하면 된다.

gdb -batch -ex 'dump binary memory instructions.bin 0x535da0 0x535da0+0x133f' ./gomixer

파일 구조는 [seed:uint32][length:uint16][body:length bytes] seed 값은 0x13579bdf, 길이는 0x1335 (4917)이다.

remap 테이블

Go_Mixer/internal/vvvv.localMap 함수는 seed를 기반으로 16개짜리 테이블을 만든다. LFSR처럼 난수를 섞어 0~10까지의 숫자를 shuffle 한 후 나머지는 0xFF로 채우는 구조였다.

1
def compute_remap(seed):
2
    s = seed & 0xFFFFFFFF
3
    arr = list(range(11))
4
    for i in range(10, 0, -1):
5
        s = ((s << 13) ^ s) & 0xFFFFFFFF
6
        s = (s ^ (s >> 7)) & 0xFFFFFFFF
7
        s = (s ^ (s << 17)) & 0xFFFFFFFF
8
        j = s % (i + 1)
9
        arr[i], arr[j] = arr[j], arr[i]
10
    return arr + [0xFF] * (16 - len(arr))

하위 nibble을 remap 테이블에 통과시켜 handler index로 사용한다. 이 테이블을 적용하지 않으면 엉뚱한 함수가 호출되어 디코딩이 틀어진다.

param 계산 규칙

opcode가 추가 파라미터를 필요로 하면 한 바이트를 더 읽는다. 이 바이트를 두 nibble로 나눠 S-box 인덱스로 사용한 뒤 seed와 xor한다.

1
low  = sbox[arg & 0xF]
2
high = sbox[arg >> 4]
3
param = (seed ^ (seed >> 7) ^ (low | (high << 4))) & 0xFFFFFFFF

param & 0xFF 는 실제 메모리 인덱스로 쓰인다. 전체 명령어를 훑어보면 인덱스는 0~127 범위에서 93개가 등장했다.

핸들러

Go 함수 이름이 난수이지만, 기능은 다음과 같다.

idx	address	desc
1	0x486b20	`mem[param & 0xFF]` push (값과 bitwise NOT 두 개를 쌍으로 저장)
2	0x486cc0	pop $\rightarrow$ nibble 치환 $\rightarrow$ MUL 상수 곱 $\rightarrow$ push
3	0x486c00	pop $\rightarrow$ `mem[param & 0xFF]`에 저장
5	0x486fa0	(flag=0) 좌회전, (flag=1) 우회전
7	0x487320	pop 두 개 $\rightarrow$ XOR

push/pop 시 값과 bitwise NOT을 함께 관리한다. XOR 해서 0xFFFFFFFF가 아니면 panic.
fdsk는 4바이트를 nibble 단위로 치환한 후 0x4E6A44B9와 곱한다.
rotate의 경우 flag는 토글 명령어 0xEE를 만나야 1이 되는데, 명령어 스트림에 0xEE가 없어서 항상 0이다.
add/multiply 등 다른 핸들러는 등록만 되어 있고 사용되지 않는다.

이제 이걸 토대로 에뮬레이터를 구성해보자.

Emulator

renmap 테이블

1
def compute_remap(seed: int) -> t.List[int]:
2
    mask = 0xFFFFFFFF
3
    state = seed & mask
4
    arr = list(range(11))
5
    for i in range(10, 0, -1):
6
        state = ((state << 13) ^ state) & mask
7
        state = (state ^ (state >> 7)) & mask
8
        state = (state ^ (state << 17)) & mask
9
        j = state % (i + 1)
10
        arr[i], arr[j] = arr[j], arr[i]
11
    return arr + [0xFF] * (16 - len(arr))

Go 바이너리의 localMap 함수를 그대로 재현했다. seed 기반 LFSR로 11개 숫자를 섞고 나머지는 0xFF로 채우는 구조다. 하위 nibble을 remap해야 handler index가 올바르게 나온다. (Remap을 무시하면 완전히 다른 함수가 호출된다.)

opcode 파싱, param 복호화

1
def load_program(path: str) -> t.List[t.Tuple[t.Union[int, str], int]]:
2
    blob = open(path, "rb").read()
3
    seed_hdr, length = struct.unpack_from("<IH", blob, 0)
4
    if seed_hdr != SEED:
5
        raise ValueError("unexpected seed header")
6
    prog = blob[6: 6 + length]
7

8
    pc = 0
9
    instructions: t.List[t.Tuple[t.Union[int, str], int]] = []
10
    while pc < len(prog):
11
        opcode = prog[pc]; pc += 1
12
        if opcode == 0xEE:
13
            instructions.append(("toggle", 0))
14
            continue
15
        if opcode == 0xF0:
16
            instructions.append(("ret", 0))
17
            break
18

19
        idx = REMAPPED[opcode & 0xF]
20
        if idx == 0xFF:
21
            raise ValueError("bad opcode")
22
        if idx in NEEDS_PARAM:
23
            arg = prog[pc]; pc += 1
24
            low = SBOX[arg & 0xF]
25
            high = SBOX[arg >> 4]
26
            param = (SEED ^ (SEED >> 7) ^ (low | (high << 4))) & 0xFFFFFFFF
27
        else:
28
            param = 0
29
        instructions.append((idx, param))
30
    return instructions

gdb로 메모리를 덤프해서 추출한 instructions.bin은 [seed][length][body] 구조다. seed가 일치하는지 검증해 안전하게 파싱한다. 파라미터는 nibble 단위 S-Box를 거친 뒤 seed와 XOR해야 Go VM과 동일한 값이 나온다. 이는 gdb에서 원본 함수 로그를 따라가며 확인했다. ![[instruction.bin.png]]

VM 실행 로직

1
def run_vm(bytes_vec: t.Sequence[BitVecRef]) -> t.List[BitVecRef]:
2
    mem: t.List[BitVecRef] = [BitVecVal(0, 32) for _ in range(128)]
3
    rev = list(reversed(bytes_vec))
4
    for index in range(16):
5
        block = rev[index * 4:(index + 1) * 4]
6
        while len(block) < 4:
7
            block.append(BitVecVal(0, 8))
8
        value = (ZeroExt(24, block[0]) << 24) \
9
            | (ZeroExt(24, block[1]) << 16) \
10
            | (ZeroExt(24, block[2]) << 8) \
11
            | ZeroExt(24, block[3])
12
        mem[32 + index] = value & BitVecVal(0xFFFFFFFF, 32)
13

14
    stack: t.List[BitVecRef] = []
15
    flag = False
16
    for opcode, param in PROGRAM:
17
        if opcode == "ret":
18
            break
19
        if opcode == "toggle":
20
            flag = not flag
21
            continue
22
        if opcode == 1:
23
            stack.append(mem[param & 0xFF])
24
        elif opcode == 2:
25
            value = stack.pop()
26
            mem[param & 0xFF] = value & BitVecVal(0xFFFFFFFF, 32)
27
        elif opcode == 3:
28
            value = stack.pop()
29
            acc = BitVecVal(0, 32)
30
            for i in range(4):
31
                byte = Extract(8 * i + 7, 8 * i, value)
32
                low = sbox4(Extract(3, 0, byte))
33
                high = sbox4(Extract(7, 4, byte))
34
                new_byte = Concat(high, low)
35
                acc = acc | (ZeroExt(24, new_byte) << (8 * i))
36
            acc = (acc * BitVecVal(MUL, 32)) & BitVecVal(0xFFFFFFFF, 32)
37
            stack.append(acc)
38
        elif opcode == 5:
39
            value = stack.pop()
40
            amt = param & 0x1F
41
            rotated = rol32(value, amt if not flag else (32 - amt))
42
            stack.append(rotated)
43
        elif opcode == 7:
44
            a = stack.pop(); b = stack.pop()
45
            stack.append(a ^ b)
46
        else:
47
            raise NotImplementedError
48
    return [mem[i] for i in range(16)]

입력을 역순으로 4바이트씩 묶어 mem[32:]에 저장하는 이유는 Go 코드에서 preloadInputBERev가 big-endian 역순으로 데이터를 적재하기 때문이다. push/pop 시 bitwise NOT 검사는 Go 런타임이 panic 여부를 확인하기 위해 사용하므로 그대로 구현했다. nibble 치환 $\rightarrow$ 곱셈 $\rightarrow$ rotate $\rightarrow$ xor 순서를 추적하여 재현했다. bytes_vec가 Z3 변수(BitVec)일 수도 있어서 ZeroExt를 사용해 정수 연산을 유지했다.

solver

1
def solve_flag() -> None:
2
    target_words = [...]
3
    flag_len = 64
4
    chars = [BitVec(f"c{i}", 8) for i in range(flag_len)]
5
    words = run_vm(chars)
6
    solver = Solver()
7
    for word_val, target in zip(words[:16], target_words):
8
        solver.add(word_val == BitVecVal(target, 32))
9
    if solver.check() != sat:
10
        print("Solver failed to find a solution.")
11
        return
12
    model = solver.model()
13
    flag_bytes = bytes(model[ch].as_long() for ch in chars)
14
    print(f"Solved flag: {flag_bytes.decode()}")

초기 시도에서는 ASCII / 길이 제약을 추가했지만 padding 때문에 unsat이 나왔다. 그래서 핵심 제약(워드 배열 일치)만 남기고 나머지는 제거했다. 길이는 넉넉히 64로 두어 padding이 잘 반영되도록 했다. 모델에서 추출한 결과 앞부분은 \x00으로 채워져 있었고, 뒤쪽 ASCII 영역이 실제 플래그였다.

6.5 sanity check 예제

1
if __name__ == "__main__":
2
    sample = b"abcd"
3
    concrete_bytes = [BitVecVal(b, 8) for b in sample]
4
    output = run_vm(concrete_bytes)
5
    print("VM output words for input 'abcd':")
6
    for idx, word in enumerate(output):
7
        simplified = simplify(word)
8
        print(f"{idx:02d}: {simplified.as_long():#010x}")
9
    solve_flag()

이렇게 실행하면 먼저 "abcd"에 대한 워드가 gdb와 일치하는지 확인하고, 바로 이어서 solver가 flag를 계산한다.

Exploit

타깃 워드 추출

정답 비교 배열은 0x531660 근처에 있다. gdb에서 바로 확인한다.

1
(gdb) x/16wx 0x531660
2
0x531660: 0x82ce0803 0xed0a0ade 0x5eb83efd 0xdd86d41a
3
0x531670: 0xc635b860 0x2115b7f1 0xf57d3092 0x17a52348
4
0x531680: 0x223c75ae 0xdf525a75 0x3773e5f4 0xfd0e81a6
5
0x531690: 0x87f325a8 0x5cd21a47 0x2290027e 0x74d1bfed

이 16개가 목표 값이다.

Solver 구성

1
flag_len = 64  # padding까지 고려해서 넉넉히 설정
2
chars = [BitVec(f"c{i}", 8) for i in range(flag_len)]
3
words = run_vm(chars)
4
for w, target in zip(words, target_words):
5
    solver.add(w == BitVecVal(target, 32))

초기에 ASCII 제약과 길이 제약을 넣었더니 unsat이 나왔다. padding 영역까지 연산에 사용되기 때문. 제약을 제거하니 즉시 해를 얻을 수 있었다.

전체 코드

1
import struct
2
import typing as t
3

4
from z3 import *
5

6
SEED = 0x13579BDF
7
MASK32 = 0xFFFFFFFF
8
SBOX = [0x03, 0x0E, 0x01, 0x0A, 0x04, 0x09, 0x05, 0x06,
9
        0x08, 0x0B, 0x0F, 0x02, 0x0D, 0x0C, 0x00, 0x07]
10
MUL = 0x4E6A44B9
11
PROGRAM_PATH = "instructions.bin"
12

13

14
def compute_remap(seed: int) -> t.List[int]:
15
    mask = MASK32
16
    state = seed & mask
17
    arr = list(range(11))
18
    for i in range(10, 0, -1):
19
        state = ((state << 13) ^ state) & mask
20
        state = (state ^ (state >> 7)) & mask
21
        state = (state ^ (state << 17)) & mask
22
        j = state % (i + 1)
23
        arr[i], arr[j] = arr[j], arr[i]
24
    return arr + [0xFF] * (16 - len(arr))
25

26

27
REMAPPED = compute_remap(SEED)
28
NEEDS_PARAM = {0, 1, 2, 5, 6, 9}
29

30

31
def load_program(path: str) -> t.List[t.Tuple[t.Union[int, str], int]]:
32
    blob = open(path, "rb").read()
33
    seed_hdr, length = struct.unpack_from("<IH", blob, 0)
34
    if seed_hdr != SEED:
35
        raise ValueError(f"unexpected seed header: {seed_hdr:#x}")
36
    prog = blob[6: 6 + length]
37

38
    pc = 0
39
    instructions: t.List[t.Tuple[t.Union[int, str], int]] = []
40
    while pc < len(prog):
41
        opcode = prog[pc]
42
        pc += 1
43

44
        if opcode == 0xEE:
45
            instructions.append(("toggle", 0))
46
            continue
47
        if opcode == 0xF0:
48
            instructions.append(("ret", 0))
49
            break
50

51
        idx = REMAPPED[opcode & 0xF]
52
        if idx == 0xFF:
53
            raise ValueError(f"opcode {opcode:#x} remapped to invalid handler")
54

55
        if idx in NEEDS_PARAM:
56
            arg = prog[pc]
57
            pc += 1
58
            low = SBOX[arg & 0xF]
59
            high = SBOX[(arg >> 4) & 0xF]
60
            sub = low | (high << 4)
61
            param = (SEED ^ (SEED >> 7) ^ sub) & MASK32
62
        else:
63
            param = 0
64
        instructions.append((idx, param))
65
    return instructions
66

67

68
PROGRAM = load_program(PROGRAM_PATH)
69

70

71
def sbox4(nibble: BitVecRef) -> BitVecRef:
72
    result = BitVecVal(SBOX[0], 4)
73
    for i in range(1, 16):
74
        result = If(nibble == BitVecVal(i, 4), BitVecVal(SBOX[i], 4), result)
75
    return result
76

77

78
def rol32(value: BitVecRef, amount: int) -> BitVecRef:
79
    amount %= 32
80
    if amount == 0:
81
        return value & BitVecVal(MASK32, 32)
82
    return ((value << amount) | LShR(value, 32 - amount)) & BitVecVal(MASK32, 32)
83

84

85
def run_vm(bytes_vec: t.Sequence[BitVecRef]) -> t.List[BitVecRef]:
86
    mem: t.List[BitVecRef] = [BitVecVal(0, 32) for _ in range(128)]
87

88
    rev = list(reversed(bytes_vec))
89
    for index in range(16):
90
        block = rev[index * 4:(index + 1) * 4]
91
        while len(block) < 4:
92
            block.append(BitVecVal(0, 8))
93
        value = (ZeroExt(24, block[0]) << 24) \
94
            | (ZeroExt(24, block[1]) << 16) \
95
            | (ZeroExt(24, block[2]) << 8) \
96
            | ZeroExt(24, block[3])
97
        mem[32 + index] = value & BitVecVal(MASK32, 32)
98

99
    stack: t.List[BitVecRef] = []
100
    flag = False
101

102
    for opcode, param in PROGRAM:
103
        if opcode == "ret":
104
            break
105
        if opcode == "toggle":
106
            flag = not flag
107
            continue
108

109
        if opcode == 1:  # load
110
            stack.append(mem[param & 0xFF])
111
        elif opcode == 2:  # store
112
            value = stack.pop()
113
            mem[param & 0xFF] = value & BitVecVal(MASK32, 32)
114
        elif opcode == 3:  # fdsk variant (nibble substitution + multiply)
115
            value = stack.pop()
116
            acc = BitVecVal(0, 32)
117
            for i in range(4):
118
                byte = Extract(8 * i + 7, 8 * i, value)
119
                low = sbox4(Extract(3, 0, byte))
120
                high = sbox4(Extract(7, 4, byte))
121
                new_byte = Concat(high, low)
122
                acc = acc | (ZeroExt(24, new_byte) << (8 * i))
123
            acc = (acc * BitVecVal(MUL, 32)) & BitVecVal(MASK32, 32)
124
            stack.append(acc)
125
        elif opcode == 5:  # rotation
126
            value = stack.pop()
127
            amt = param & 0x1F
128
            rotated = rol32(value, amt if not flag else (32 - amt))
129
            stack.append(rotated)
130
        elif opcode == 7:  # xor
131
            a = stack.pop()
132
            b = stack.pop()
133
            stack.append(a ^ b)
134
        else:
135
            raise NotImplementedError(f"Unhandled opcode index {opcode}")
136

137
    return [mem[i] for i in range(16)]
138

139

140
def main() -> None:
141
    # sanity-check: emulate using concrete ASCII bytes "abcd"
142
    sample = b"abcd"
143
    concrete_bytes: t.List[BitVecRef] = [BitVecVal(b, 8) for b in sample]
144
    output = run_vm(concrete_bytes)
145
    print("VM output words for input 'abcd':")
146
    for idx, word in enumerate(output):
147
        simplified = simplify(word)
148
        if is_bv_value(simplified):
149
            value = simplified.as_long()
150
            print(f"{idx:02d}: {value:#010x}")
151
        else:
152
            print(f"{idx:02d}: {simplified}")
153

154

155
def solve_flag() -> None:
156
    target_words = [
157
        0x82CE0803, 0xED0A0ADE, 0x5EB83EFD, 0xDD86D41A,
158
        0xC635B860, 0x2115B7F1, 0xF57D3092, 0x17A52348,
159
        0x223C75AE, 0xDF525A75, 0x3773E5F4, 0xFD0E81A6,
160
        0x87F325A8, 0x5CD21A47, 0x2290027E, 0x74D1BFED,
161
    ]
162

163
    flag_len = 64
164
    chars = [BitVec(f"c{i}", 8) for i in range(flag_len)]
165
    padded_input: t.List[BitVecRef] = chars + [BitVecVal(0, 8) for _ in range(64 - flag_len)]
166

167
    words = run_vm(padded_input)
168

169
    solver = Solver()
170

171
    for word_val, target in zip(words[:16], target_words):
172
        solver.add(simplify(word_val) == BitVecVal(target, 32))
173

174
    if solver.check() != sat:
175
        print("Solver failed to find a solution.")
176
        return
177

178
    model = solver.model()
179
    flag_bytes = bytes(model[ch].as_long() for ch in chars)
180
    print(f"Solved flag: {flag_bytes.decode()}")
181

182

183
if __name__ == "__main__":
184
    main()
185
    solve_flag()

실행 결과

1
andsopwn@meow:~/ctftemp/hspace/rev/gomixer$ python3 vm_solver.py
2
VM output words for input 'abcd':
3
00: 0x354e4c3a
4
01: 0x95b11f95
5
02: 0xc3854e0b
6
03: 0xf7dd4eb1
7
04: 0x23a9583c
8
05: 0xb8ef8d79
9
06: 0x82d967b8
10
07: 0xaa56bd40
11
08: 0x0fbf5fad
12
09: 0xdbbd1af3
13
10: 0x67a236f0
14
11: 0xc604dab0
15
12: 0x86246b49
16
13: 0x473f3e13
17
14: 0x949e7ce2
18
15: 0xa0e5cb7f
19
Solved flag: hspace{yeah_y0u_h4v3_br0ken_g0_vm_h4ha_thats_it_gggg}

[CLUB LEAGUE] Go Mixer writeup