Reverse#

baby-rev#

Question Source Code

1
#!/usr/bin/env python3
2
T = bytes.fromhex("7066444d5033220a5b08d6a2fcc38ca7a788c2a17b6a15554d78341b")
3

4
flag = input("flag: ")
5
if len(flag) == len(T) and all(
6
    ord(flag[i]) ^ ((i * 13 + 7) & 0xFF) == T[i] for i in range(len(T))
7
):
8
    print("correct!")
9
else:
10
    print("nope")

There’s nothing much to say, just directly reverse one step back, so easy

1
#!/usr/bin/env python3
2
T = bytes.fromhex("7066444d5033220a5b08d6a2fcc38ca7a788c2a17b6a15554d78341b")
3

4
def main():
5
    flag = "".join(chr(b ^ ((i * 13 + 7) & 0xFF)) for i, b in enumerate(T))
6
    print(flag)
7

8
if __name__ == "__main__":
9
    main()

wreck{wh4t_4_s1mpl3_pr0gr4m}

pipeline#

The problem essentially involves feeding the input 32 ByteDance flag into _Q’s 32 transformations, and finally requiring the result to equal _T

Most operations are clearly reversible

_0: XOR by key, and the inverse operation is still itself
_1: Add by key, and the inverse operation is subtract
_2: Subtract by key, and the inverse operation is addition
_3: Circular left shift, and its inverse operation is circular right shift
_4: Permutation, and its inverse operation is inverse permutation
_5: S-box substitution, and the inverse operation is reverse lookup table
_6: reverse, the inverse operation is still itself
_7: Swap the front and back halves, and the inverse operation is still itself
_8: Prefix XOR, the inverse operation satisfies orig[i] = out[i] ^ out[i - 1]
_9: Just find the multiplicative inverse modulo 256 by multiplying with an odd constant

What is truly less straightforward is _A and _B

1
c = bytes(x[i:i + 3])
2
d = hash(c).digest()[:3]
3
x[i:i + 3] = bytes(p ^ q for p, q in zip(c, d))

They only affect 3 consecutive ByteDance, so when reaching the corresponding position during the reverse process, all 2^24 possible inputs can be enumerated for the current target 3 ByteDance to find the ones that satisfy

1
chunk ^ hash(chunk)[:3] == target

preimage

There are two key pieces of information here

_B has only one preimage for the target f51d49: 4c94db
_A’s target cfafe4 has three preimages:
79335e
a44c66
e28388

Bringing these three candidates back to the entire inverse chain respectively, only e28388 can ultimately restore a valid flag that satisfies _c().

1
#!/usr/bin/env python3
2
import hashlib
3
import random
4

5
def g(seed, n):
6
    r = random.Random(seed)
7
    arr = list(range(n))
8
    r.shuffle(arr)
9
    return arr
10

11
S = g(0xBEEF1234, 256)
12
P = g(0xCAFEBABE, 32)
13
T = bytes.fromhex("34ad7a3e4331511d979f075ee8b4619a1aaee35184cb1f1d933e948631ec9f8e")
14

15
def xor_bytes(x, k):
16
    for i in range(len(x)):
17
        x[i] ^= k[i % len(k)]
18

19
def add_bytes(x, k):
20
    for i in range(len(x)):
21
        x[i] = (x[i] + k[i % len(k)]) & 0xFF
22

23
def sub_bytes(x, k):
24
    for i in range(len(x)):
25
        x[i] = (x[i] - k[i % len(k)]) & 0xFF
26

27
def rol_bytes(x, a):
28
    a &= 7
29
    if not a:
30
        return
31
    for i, b in enumerate(x):
32
        x[i] = ((b << a) | (b >> (8 - a))) & 0xFF
33

34
def ror_bytes(x, a):
35
    a &= 7
36
    if not a:
37
        return
38
    for i, b in enumerate(x):
39
        x[i] = ((b >> a) | ((b << (8 - a)) & 0xFF)) & 0xFF
40

41
def permute(x, p):
42
    out = bytearray(len(x))
43
    for i, j in enumerate(p):
44
        out[i] = x[j]
45
    x[:] = out
46

47
def inv_permute(x, p):
48
    out = bytearray(len(x))
49
    for i, j in enumerate(p):
50
        out[j] = x[i]
51
    x[:] = out
52

53
def sbox(x, table):
54
    for i in range(len(x)):
55
        x[i] = table[x[i]]
56

57
def inv_sbox(x, table):
58
    inv = [0] * 256
59
    for i, v in enumerate(table):
60
        inv[v] = i
61
    for i in range(len(x)):
62
        x[i] = inv[x[i]]
63

64
def rev(x):
65
    x.reverse()
66

67
def half_swap(x):
68
    n = len(x) // 2
69
    left = bytes(x[:n])
70
    x[:n] = x[n:]
71
    x[n:] = left
72

73
def prefix_xor(x):
74
    for i in range(1, len(x)):
75
        x[i] ^= x[i - 1]
76

77
def inv_prefix_xor(x):
78
    out = bytearray(len(x))
79
    out[0] = x[0]
80
    for i in range(1, len(x)):
81
        out[i] = x[i] ^ x[i - 1]
82
    x[:] = out
83

84
def mul_bytes(x, k):
85
    for i in range(len(x)):
86
        x[i] = (x[i] * k[i % len(k)]) & 0xFF
87

88
def inv_mul_bytes(x, k):
89
    invk = [pow(v, -1, 256) for v in k]
90
    for i in range(len(x)):
91
        x[i] = (x[i] * invk[i % len(invk)]) & 0xFF
92

93
def hash_mix(x, idx, algo):
94
    chunk = bytes(x[idx : idx + 3])
95
    d = getattr(hashlib, algo)(chunk).digest()[:3]
96
    x[idx : idx + 3] = bytes(a ^ b for a, b in zip(chunk, d))
97

98
def brute_hash_preimages(algo, target3):
99
    res = []
100
    h = getattr(hashlib, algo)
101
    for v in range(1 << 24):
102
        chunk = v.to_bytes(3, "big")
103
        d = h(chunk).digest()[:3]
104
        if bytes(a ^ b for a, b in zip(chunk, d)) == target3:
105
            res.append(chunk)
106
    return res
107

108
OPS = [
109
    ("xor", b"BUZZBUZZ"),
110
    ("add", b"\x12\x34\x56\x78\x9a\xbc\xde\xf0"),
111
    ("rol", 3),
112
    ("sbox", S),
113
    ("perm", P),
114
    ("pxor", None),
115
    ("sub", b"\x42\x13\x37\x99"),
116
    ("swap", None),
117
    ("xor", b"\xab\xcd\xef\x12"),
118
    ("mul", [3, 5, 7, 11]),
119
    ("rol", 2),
120
    ("sbox", S),
121
    ("rev", None),
122
    ("add", b"\x01\x02\x03\x04"),
123
    ("md5", 4),
124
    ("perm", P),
125
    ("xor", b"\x55\xaa\x55\xaa"),
126
    ("rol", 1),
127
    ("sbox", S),
128
    ("sub", b"\x11\x22\x33\x44"),
129
    ("pxor", None),
130
    ("swap", None),
131
    ("mul", [3, 11, 13, 17]),
132
    ("sha256", 12),
133
    ("perm", P),
134
    ("rev", None),
135
    ("xor", b"\xf0\x0d\xca\xfe"),
136
    ("add", b"\x77\x88\x99\xaa"),
137
    ("mul", [5, 9, 11, 13]),
138
    ("rol", 4),
139
    ("sbox", S),
140
    ("sub", b"\x99\x55\x33\x11"),
141
]
142

143
def apply_op(x, op):
144
    typ, arg = op
145
    if typ == "xor":
146
        xor_bytes(x, arg)
147
    elif typ == "add":
148
        add_bytes(x, arg)
149
    elif typ == "sub":
150
        sub_bytes(x, arg)
151
    elif typ == "rol":
152
        rol_bytes(x, arg)
153
    elif typ == "perm":
154
        permute(x, arg)
155
    elif typ == "sbox":
156
        sbox(x, arg)
157
    elif typ == "rev":
158
        rev(x)
159
    elif typ == "swap":
160
        half_swap(x)
161
    elif typ == "pxor":
162
        prefix_xor(x)
163
    elif typ == "mul":
164
        mul_bytes(x, arg)
165
    elif typ in ("md5", "sha256"):
166
        hash_mix(x, arg, typ)
167
    else:
168
        raise ValueError(typ)
169

170
def check(flag):
171
    if not (flag.startswith(b"wreck{") and flag.endswith(b"}")):
172
        return False
173
    if not all(0x20 <= c <= 0x7E for c in flag):
174
        return False
175
    x = bytearray(flag)
176
    for op in OPS:
177
        apply_op(x, op)
178
    return bytes(x) == T
179

180
def apply_inv_block(x, block):
181
    for typ, arg in block:
182
        if typ == "xor":
183
            xor_bytes(x, arg)
184
        elif typ == "add":
185
            sub_bytes(x, arg)
186
        elif typ == "sub":
187
            add_bytes(x, arg)
188
        elif typ == "rol":
189
            ror_bytes(x, arg)
190
        elif typ == "perm":
191
            inv_permute(x, arg)
192
        elif typ == "sbox":
193
            inv_sbox(x, arg)
194
        elif typ == "rev":
195
            rev(x)
196
        elif typ == "swap":
197
            half_swap(x)
198
        elif typ == "pxor":
199
            inv_prefix_xor(x)
200
        elif typ == "mul":
201
            inv_mul_bytes(x, arg)
202
        else:
203
            raise ValueError(typ)
204

205
def solve():
206
    x = bytearray(T)
207

208
    tail = [
209
        ("sub", b"\x99\x55\x33\x11"),
210
        ("sbox", S),
211
        ("rol", 4),
212
        ("mul", [5, 9, 11, 13]),
213
        ("add", b"\x77\x88\x99\xaa"),
214
        ("xor", b"\xf0\x0d\xca\xfe"),
215
        ("rev", None),
216
        ("perm", P),
217
    ]
218
    apply_inv_block(x, tail)
219

220
    b_candidates = brute_hash_preimages("sha256", bytes(x[12:15]))
221
    assert len(b_candidates) == 1
222
    x[12:15] = b_candidates[0]
223

224
    mid = [
225
        ("mul", [3, 11, 13, 17]),
226
        ("swap", None),
227
        ("pxor", None),
228
        ("sub", b"\x11\x22\x33\x44"),
229
        ("sbox", S),
230
        ("rol", 1),
231
        ("xor", b"\x55\xaa\x55\xaa"),
232
        ("perm", P),
233
    ]
234
    apply_inv_block(x, mid)
235

236
    a_candidates = brute_hash_preimages("md5", bytes(x[4:7]))
237

238
    head = [
239
        ("add", b"\x01\x02\x03\x04"),
240
        ("rev", None),
241
        ("sbox", S),
242
        ("rol", 2),
243
        ("mul", [3, 5, 7, 11]),
244
        ("xor", b"\xab\xcd\xef\x12"),
245
        ("swap", None),
246
        ("sub", b"\x42\x13\x37\x99"),
247
        ("pxor", None),
248
        ("perm", P),
249
        ("sbox", S),
250
        ("rol", 3),
251
        ("add", b"\x12\x34\x56\x78\x9a\xbc\xde\xf0"),
252
        ("xor", b"BUZZBUZZ"),
253
    ]
254

255
    for a in a_candidates:
256
        y = bytearray(x)
257
        y[4:7] = a
258
        apply_inv_block(y, head)
259
        if check(bytes(y)):
260
            return bytes(y)
261

262
    raise RuntimeError("flag not found")
263

264
if __name__ == "__main__":
265
    print(solve().decode())

wreck{h4shing_1n_my_p1p3l1n3???}

gotohell-1#

First look at main

The input length must be 39.

The end does not involve byte-by-byte comparison; instead, it first runs a large segment of arithmetic/XOR obfuscation, and finally checks several sets of 32-bit states:

1
if ( v16 != -2103969039 )
2
  goto LABEL_55;
3

4
if ( v15 == -1082669001
5
  && n722405961 == 722405961
6
  && v13 == -2111249330
7
  && n1525289352 == 1525289352
8
  && v10 == -309151393
9
  && n1504177626 == 1504177626 )

Although there are many branches in the middle, most of them only depend on a few blocks after the input is treated as a 32-bit little-endian integer:

s corresponds to the first 4 ByteDance

v19 corresponds to Bytes 5 to 8

v27 corresponds to the last 3 ByteDance

The flag format is wreck{...} Subsequent consideration of constrained blasting

After wreck{ is stuffed into the first few 32-bit blocks in little-endian, many bit judgments will be directly fixed:

(s & 0x04000000)!= 0 is false

(s & 0x00000100)!= 0 is false

(s & 0x00000020)!= 0 is true

(s & 0x00000400)!= 0 is false

(v19 & 0x200)!= 0 is true

(v19 & 0x20)!= 0 is true

(v19 & 8)!= 0 is true

(v19 & 0x80) == 0 is true

Additionally, since the end must be }, the corresponding position of v27 will also be fixed, so the main chain only has one feasible and successful path left.

It has changed from a messy goto obfuscation to a fixed single path, and then collected the bit vector expressions on the path

Request the remaining 33 characters

1
from __future__ import annotations
2

3
import json
4
import re
5
import time
6

7
import z3
8
from pysat.solvers import Cadical153
9

10
# These 12 branch decisions are fixed once you know the format is `wreck{...}`.
11
FIXED_PATH = [
12
    False,  # (s & 0x04000000) != 0
13
    True,   # (v19 & 0x200) != 0
14
    False,  # (s & 0x100) != 0
15
    True,   # (v19 & 0x20) != 0
16
    True,   # (v19 & 8) != 0
17
    True,   # (s & 0x20) != 0
18
    True,   # (v27 & 0x400000) != 0
19
    True,   # (v19 & 0x80) == 0
20
    False,  # (s & 0x400) != 0
21
    True,   # (s & 0x20000000) != 0
22
    False,  # (s & 0x10000000) != 0
23
    False,  # (s & 0x08000000) != 0
24
]
25

26
ALPHABET = "abcdefghijklmnopqrstuvwxyz0123456789_{}"
27

28
def normalize(text: str) -> str:
29
    return re.sub(r"\s+", " ", text.replace("\n", " ")).strip()
30

31
def split_and(expr: str) -> list[str]:
32
    parts: list[str] = []
33
    depth = 0
34
    cur: list[str] = []
35
    i = 0
36
    while i < len(expr):
37
        ch = expr[i]
38
        if ch == "(":
39
            depth += 1
40
        elif ch == ")":
41
            depth -= 1
42
        if depth == 0 and expr.startswith("&&", i):
43
            parts.append("".join(cur).strip())
44
            cur = []
45
            i += 2
46
            continue
47
        cur.append(ch)
48
        i += 1
49
    if cur:
50
        parts.append("".join(cur).strip())
51
    return parts
52

53
class MiniCParser:
54
    def __init__(self, text: str):
55
        self.text = text
56
        self.i = 0
57

58
    def skip_ws(self) -> None:
59
        while self.i < len(self.text) and self.text[self.i].isspace():
60
            self.i += 1
61

62
    def starts(self, token: str) -> bool:
63
        return self.text.startswith(token, self.i)
64

65
    def read_paren(self) -> str:
66
        assert self.text[self.i] == "("
67
        depth = 0
68
        start = self.i + 1
69
        while self.i < len(self.text):
70
            ch = self.text[self.i]
71
            if ch == "(":
72
                depth += 1
73
            elif ch == ")":
74
                depth -= 1
75
                if depth == 0:
76
                    out = self.text[start:self.i]
77
                    self.i += 1
78
                    return out
79
            self.i += 1
80
        raise ValueError("unclosed parenthesis")
81

82
    def read_stmt(self):
83
        self.skip_ws()
84
        if self.i >= len(self.text):
85
            return None
86

87
        if self.starts("if"):
88
            self.i += 2
89
            self.skip_ws()
90
            cond = self.read_paren().strip()
91
            then_node = self.read_stmt()
92
            self.skip_ws()
93
            else_node = None
94
            if self.starts("else"):
95
                self.i += 4
96
                else_node = self.read_stmt()
97
            return ("if", cond, then_node, else_node)
98

99
        if self.text[self.i] == "{":
100
            self.i += 1
101
            body = []
102
            while True:
103
                self.skip_ws()
104
                if self.text[self.i] == "}":
105
                    self.i += 1
106
                    return ("block", body)
107
                body.append(self.read_stmt())
108

109
        if self.starts("goto LABEL_55"):
110
            j = self.text.index(";", self.i)
111
            self.i = j + 1
112
            return ("goto_fail",)
113

114
        if self.starts("LABEL_55:"):
115
            self.i += len("LABEL_55:")
116
            return ("label", "LABEL_55")
117

118
        j = self.text.index(";", self.i)
119
        stmt = self.text[self.i:j].strip()
120
        self.i = j + 1
121
        return ("stmt", stmt)
122

123
def load_main_tail():
124
    data = json.load(open(".ida_main_full.json", "r", encoding="utf-8"))["code"]
125
    data = re.sub(r"/**\***.*?**\***/", "", data, flags=re.S)
126
    data = re.sub(r"(0x[0-9A-Fa-f]+|\d+)([uUlL]+)\b", r"\1", data)
127

128
    start = data.index("v12 = ((v23")
129
    final_if = data.index("if ( v15 == -1082669001")
130
    end = data.index("{", final_if)
131
    text = data[start:end]
132

133
    parser = MiniCParser(text)
134
    ast = []
135
    while True:
136
        node = parser.read_stmt()
137
        if node is None:
138
            return ast
139
        ast.append(node)
140

141
def build_constraints(ast):
142
    words = [z3.BitVec(f"x{i}", 32) for i in range(10)]
143
    values = {
144
        "s": words[0],
145
        "v19": words[1],
146
        "v20": words[2],
147
        "n1504177626_1": words[3],
148
        "v22": words[4],
149
        "v23": words[5],
150
        "v24": words[6],
151
        "v25": words[7],
152
        "n1525289352_1": words[8],
153
        "v27": words[9],
154
        "stdout": z3.BitVecVal(0, 64),
155
        "stdin": z3.BitVecVal(0, 64),
156
    }
157
    for name in [
158
        "v8",
159
        "n1504177626",
160
        "v10",
161
        "n1525289352",
162
        "v12",
163
        "v13",
164
        "n722405961",
165
        "v15",
166
        "v16",
167
        "v17",
168
    ]:
169
        values[name] = None
170

171
    def eval_expr(expr: str, env: dict):
172
        return eval(normalize(expr), {"__builtins__": None}, {k: v for k, v in env.items() if v is not None})
173

174
    def eval_cond(cond: str, env: dict):
175
        cond = normalize(cond)
176
        pieces = split_and(cond)
177
        if len(pieces) > 1:
178
            return z3.And(*[eval_cond(piece, env) for piece in pieces])
179
        return eval_expr(cond, env)
180

181
    class State:
182
        def __init__(self):
183
            self.env = dict(values)
184
            self.constraints = []
185
            self.done = False
186

187
    def walk(node, state: State, branch_idx: int):
188
        kind = node[0]
189

190
        if kind == "block":
191
            for sub in node[1]:
192
                state, branch_idx = walk(sub, state, branch_idx)
193
            return state, branch_idx
194

195
        if kind == "stmt":
196
            text = normalize(node[1])
197

198
            if re.match(r"^[A-Za-z_][A-Za-z0-9_]*\s***\(**.***\)**$", text):
199
                return state, branch_idx
200

201
            if text.startswith("return "):
202
                state.done = True
203
                return state, branch_idx
204

205
            m = re.match(r"^([A-Za-z_][A-Za-z0-9_]*)\s*([**\^\+\-**]?=)\s*(.*)$", text)
206
            if m:
207
                name, op, expr = m.groups()
208
                rhs = eval_expr(expr, state.env)
209
                cur = state.env.get(name)
210
                if op == "=":
211
                    state.env[name] = rhs
212
                elif op == "+=":
213
                    state.env[name] = cur + rhs
214
                elif op == "-=":
215
                    state.env[name] = cur - rhs
216
                elif op == "^=":
217
                    state.env[name] = cur ^ rhs
218
            return state, branch_idx
219

220
        if kind == "if":
221
            cond, then_node, else_node = node[1], node[2], node[3]
222

223
            if "v15 == -1082669001" in cond and "n722405961 == 722405961" in cond:
224
                state.constraints.append(eval_cond(cond, state.env))
225
                state.done = True
226
                return state, branch_idx
227

228
            if then_node[0] == "goto_fail" and else_node is None:
229
                state.constraints.append(z3.Not(eval_cond(cond, state.env)))
230
                return state, branch_idx
231

232
            take_then = FIXED_PATH[branch_idx]
233
            branch_idx += 1
234
            test = eval_cond(cond, state.env)
235
            state.constraints.append(test if take_then else z3.Not(test))
236
            return walk(then_node if take_then else else_node, state, branch_idx)
237

238
        return state, branch_idx
239

240
    state = State()
241
    branch_idx = 0
242
    for node in ast:
243
        state, branch_idx = walk(node, state, branch_idx)
244
        if state.done:
245
            break
246

247
    return words, state.constraints
248

249
def add_flag_shape_constraints(goal: z3.Goal, words) -> None:
250
    for i in range(10):
251
        bit_limit = 24 if i == 9 else 32
252
        for bit in range(bit_limit):
253
            alias = z3.Bool(f"x{i}_b{bit}")
254
            goal.add(alias == (z3.Extract(bit, bit, words[i]) == 1))
255

256
    goal.add(z3.Extract(31, 24, words[9]) == 0)
257

258
    for idx, ch in enumerate(b"wreck{"):
259
        word_id = idx // 4
260
        shift = (idx % 4) * 8
261
        goal.add(z3.Extract(shift + 7, shift, words[word_id]) == ch)
262

263
    goal.add(z3.Extract(23, 16, words[9]) == ord("}"))
264

265
    alphabet = [ord(c) for c in ALPHABET]
266
    for i in range(39):
267
        word_id = i // 4
268
        shift = (i % 4) * 8
269
        byte = z3.Extract(shift + 7, shift, words[word_id])
270
        goal.add(z3.Or(*[byte == c for c in alphabet]))
271

272
def cnf_from_goal(goal: z3.Goal):
273
    cnf = z3.Then("simplify", "bit-blast", "aig", "tseitin-cnf")(goal)[0]
274

275
    varmap: dict[str, int] = {}
276
    clauses: list[list[int]] = []
277

278
    def lit_to_int(lit) -> int:
279
        sign = 1
280
        if z3.is_not(lit):
281
            sign = -1
282
            lit = lit.arg(0)
283
        name = lit.decl().name()
284
        if name not in varmap:
285
            varmap[name] = len(varmap) + 1
286
        return sign * varmap[name]
287

288
    for formula in cnf:
289
        if z3.is_or(formula):
290
            clauses.append([lit_to_int(child) for child in formula.children()])
291
        else:
292
            clauses.append([lit_to_int(formula)])
293

294
    return varmap, clauses
295

296
def decode_model(model: set[int], varmap: dict[str, int]) -> str:
297
    out = []
298
    for i in range(39):
299
        word_id = i // 4
300
        bitoff = (i % 4) * 8
301
        byte = 0
302
        for j in range(8):
303
            name = f"x{word_id}_b{bitoff + j}"
304
            if varmap.get(name, 0) in model:
305
                byte |= 1 << j
306
        out.append(byte)
307
    return bytes(out).decode()
308

309
def recover_flag() -> str:
310
    ast = load_main_tail()
311
    words, path_constraints = build_constraints(ast)
312

313
    goal = z3.Goal()
314
    add_flag_shape_constraints(goal, words)
315
    goal.add(*path_constraints)
316

317
    varmap, clauses = cnf_from_goal(goal)
318
    with Cadical153(bootstrap_with=clauses) as solver:
319
        if not solver.solve():
320
            raise RuntimeError("solver returned UNSAT")
321
        model_data = solver.get_model()
322
        if model_data is None:
323
            raise RuntimeError("solver did not return a model")
324
        model = {v for v in model_data if v > 0}
325
    return decode_model(model, varmap)
326

327
if __name__ == "__main__":
328
    start = time.time()
329
    flag = recover_flag()
330
    print(flag)
331
    print(f"[+] solved in {time.time() - start:.2f}s")

wreck{n0w_h34d3d_t0_3xtr4_h3ll_8b2f4e9}