TL;DR

64바이트 입력을 16개의 16비트 word로 big-endian 변환 후 계산한다.
모든 산술은 0x10000 모듈러 환경이라 연산 결과를 BitVec(16)으로 추적해야 한다.
목표 워드 테이블과 동일하게 만들기 위해 Z3로 역연산을 구성했고, ASCII 제약을 추가해 플래그 문자열을 복원했다.

opcodes

Analysis

데이터 흐름

주 로직은 IDA 기준 sub_140016190. 입력 64바이트는 v13[16:80]에 저장된 뒤 2바이트씩 묶여 v16~v47에 배치된다.

1
for (int k = 0; k < 32; ++k)
2
  w[k] = (v13[2 * k + 16] << 8) | v13[2 * k + 17];

상위 바이트가 앞서므로 big-endian을 그대로 재현해야 한다. 이후 모든 연산은 16비트 레지스터에서 이루어지므로 & 0xFFFF 또는 BitVec(16) 환경을 유지해야 한다.

목표 워드

최종 판별은 v16~v47이 미리 하드코딩된 값 v49와 일치하는지 확인하는 방식이다. 디버거나 디컴파일러로 v49 테이블을 덤프해두면 역산 준비가 끝난다.

[37579, 61717, 17610, 18733, 29327, 62894, 40252, 23200,
 23625, 11321, 14689, 23134, 55867, 39558, 49656, 29290,
 12786,  8829, 42613, 36754, 14134, 27522,  8742, 21858,
 65392, 15348, 37595, 30308,  8751,  3344, 14842, 34102]

Exploit

모델링

각 워드는 상·하위 바이트 두 개로 구성되므로, solver에서 BitVec(8) 두 개를 ZeroExt 후 결합했다. 이후 바이너리에서 관찰한 연산 순서를 그대로 재현한다.

1
from z3 import *
2

3
w = [BitVec(f"w{i}", 16) for i in range(32)]
4
hi = [BitVec(f"hi{i}", 8) for i in range(32)]
5
lo = [BitVec(f"lo{i}", 8) for i in range(32)]
6

7
s = Solver()
8
for i in range(32):
9
    s.add(w[i] == (ZeroExt(8, hi[i]) << 8) | ZeroExt(8, lo[i]))
10

11
v16, v17, v18, v19, v20, v21, v22, v23 = w[0:8]
12
v24, v25, v26, v27, v28, v29, v30, v31 = w[8:16]
13
v32, v33, v34, v35, v36, v37, v38, v39 = w[16:24]
14
v40, v41, v42, v43, v44, v45, v46, v47 = w[24:32]
15

16
v16 = v23 ^ v34 ^ (v45 + v16)
17
v17 = v32 ^ (7 * v17)
18
v18 = v16 + v18 - v45 - v45
19
v19 = v19 - v38
20
v20 = (v35 - v31) ^ v32 ^ (v30 + 3 * v20)
21
v21 = v21 ^ (v16 + v42 - v40)
22
v22 = v22 ^ ((v42 - v44 - v41) ^ v41)
23
v23 = v40 ^ (v30 + v23 - v46)
24
v24 = (v25 + v29) ^ (v24 - v26 - v42)
25
v25 = v42 + v25 - v32
26
v27 = v27 ^ (2 * v34)
27
v28 = v37 + 3 * v28 - v20 - v18
28
v29 = v29 - 4 * v38
29
v30 = v43 ^ (v30 - v18)
30
v31 = v31 * 2
31
v32 = v32 ^ (v32 + 3 * v29)
32
v33 = v33 ^ (v43 - v17)
33
v34 = v36 + v34 - v30
34
v35 = v35 + 2 * v42 - v36
35
v37 = v37 ^ (3 * v23)
36
v38 = v38 ^ ((2 * v34) ^ (v36 - v28))
37
v39 = v39 + v30 + v45
38
v40 = v40 ^ ((v21 + v27) ^ (v40 + v34 - v26))
39
v41 = v41 ^ (v43 - v35 - v22)
40
v42 = v35 ^ (v42 - v26 - 3 * v19)
41
v43 = v43 ^ (6 * v34 + v24)
42
v44 = v44 ^ (3 * v24 + v40)
43
v45 = v45 - v44 - v32
44
v46 = v22 ^ (v20 + v46)
45
v47 = v47 ^ (v28 + v45)
46

47
vt = [v16, v17, v18, v19, v20, v21, v22, v23,
48
      v24, v25, v26, v27, v28, v29, v30, v31,
49
      v32, v33, v34, v35, v36, v37, v38, v39,
50
      v40, v41, v42, v43, v44, v45, v46, v47]
51

52
for expect, val in zip(vt, v49):
53
    s.add(expect == BitVecVal(val, 16))

제약 조건

ASCII 플래그 형태를 강제하기 위해 0x20~0x7E 범위를 제한하고, 접두사와 닫는 중괄호만 고정했다.

1
for i in range(32):
2
    s.add(And(hi[i] >= 0x20, hi[i] <= 0x7E))
3
    s.add(And(lo[i] >= 0x20, lo[i] <= 0x7E))
4

5
s.add(hi[0] == ord('f'))
6
s.add(lo[0] == ord('i'))
7
s.add(hi[1] == ord('e'))
8
s.add(lo[1] == ord('s'))
9
s.add(hi[2] == ord('t'))
10
s.add(lo[2] == ord('a'))
11
s.add(hi[3] == ord('{'))
12
s.add(lo[31] == ord('}'))

모델을 꺼내면서 상·하위 바이트를 번갈아 붙이면 원래 64바이트 입력이 복원된다.

solver output

Flag

fiesta{dfcfff1df4e189a80dfcb9e9570f317bf76db2729143a215c6da127b}

[FIESTA 2025] Binary Fuzzle writeup