Rating: 3.0
# TSG CTF 2023 - rev/beginners_rev_2023
## Solution
Ghidra decompiled it well, so I just used z3.
```python
import z3
s = z3.Solver()
map3 = bytes.fromhex("""
00 00 00 00 00 00 00 00 32 00 00 00 63 00 00 00
4f 00 00 00 6a 00 00 00 61 00 00 00 0b 00 00 00
d7 00 00 00 31 00 00 00 76 00 00 00 29 00 00 00
0c 00 00 00 69 00 00 00 21 00 00 00 93 00 00 00
1c 00 00 00 2b 00 00 00 e9 00 00 00 b6 00 00 00
aa 00 00 00 3c 00 00 00 ca 00 00 00 07 00 00 00
9b 00 00 00 54 00 00 00 58 00 00 00 06 00 00 00
ed 00 00 00 96 00 00 00 89 00 00 00 c7 00 00 00
f9 00 00 00 66 00 00 00 b8 00 00 00 92 00 00 00
82 00 00 00 17 00 00 00 19 00 00 00 1d 00 00 00
a9 00 00 00 30 00 00 00 fc 00 00 00 e4 00 00 00
f7 00 00 00 33 00 00 00 5c 00 00 00 bb 00 00 00
8c 00 00 00 7a 00 00 00 dd 00 00 00 38 00 00 00
48 00 00 00 cd 00 00 00 01 00 00 00 1b 00 00 00
b3 00 00 00 de 00 00 00 00 00 00 00 15 00 00 00
ce 00 00 00 43 00 00 00 03 00 00 00 7e 00 00 00
36 00 00 00 7d 00 00 00 23 00 00 00 73 00 00 00
6b 00 00 00 b1 00 00 00 46 00 00 00 52 00 00 00
59 00 00 00 3d 00 00 00 7f 00 00 00 5b 00 00 00
78 00 00 00 9f 00 00 00 85 00 00 00 4a 00 00 00
20 00 00 00 97 00 00 00 9a 00 00 00 1f 00 00 00
77 00 00 00 ab 00 00 00 28 00 00 00 72 00 00 00
cb 00 00 00 81 00 00 00 cc 00 00 00 eb 00 00 00
d2 00 00 00 b9 00 00 00 2d 00 00 00 12 00 00 00
13 00 00 00 c0 00 00 00 a6 00 00 00 25 00 00 00
71 00 00 00 0a 00 00 00 88 00 00 00 9e 00 00 00
37 00 00 00 22 00 00 00 24 00 00 00 47 00 00 00
42 00 00 00 a5 00 00 00 fa 00 00 00 2a 00 00 00
53 00 00 00 8a 00 00 00 6c 00 00 00 99 00 00 00
09 00 00 00 e3 00 00 00 ef 00 00 00 ec 00 00 00
e0 00 00 00 a0 00 00 00 51 00 00 00 f3 00 00 00
1e 00 00 00 04 00 00 00 8f 00 00 00 e7 00 00 00
02 00 00 00 a1 00 00 00 90 00 00 00 60 00 00 00
a4 00 00 00 ad 00 00 00 fd 00 00 00 5f 00 00 00
79 00 00 00 44 00 00 00 6e 00 00 00 39 00 00 00
34 00 00 00 4c 00 00 00 a3 00 00 00 d4 00 00 00
74 00 00 00 b4 00 00 00 9c 00 00 00 8e 00 00 00
83 00 00 00 e6 00 00 00 4e 00 00 00 d5 00 00 00
3a 00 00 00 f1 00 00 00 be 00 00 00 6d 00 00 00
05 00 00 00 ba 00 00 00 84 00 00 00 b2 00 00 00
87 00 00 00 10 00 00 00 f4 00 00 00 bc 00 00 00
d8 00 00 00 fe 00 00 00 ae 00 00 00 bd 00 00 00
7c 00 00 00 c3 00 00 00 e8 00 00 00 e5 00 00 00
4b 00 00 00 c9 00 00 00 2c 00 00 00 b5 00 00 00
3f 00 00 00 4d 00 00 00 50 00 00 00 bf 00 00 00
8d 00 00 00 45 00 00 00 c8 00 00 00 18 00 00 00
f0 00 00 00 da 00 00 00 8b 00 00 00 db 00 00 00
c4 00 00 00 16 00 00 00 08 00 00 00 0f 00 00 00
62 00 00 00 d6 00 00 00 91 00 00 00 1a 00 00 00
a8 00 00 00 9d 00 00 00 d1 00 00 00 98 00 00 00
86 00 00 00 67 00 00 00 c5 00 00 00 68 00 00 00
c6 00 00 00 35 00 00 00 af 00 00 00 ea 00 00 00
f8 00 00 00 c2 00 00 00 d0 00 00 00 56 00 00 00
94 00 00 00 40 00 00 00 ff 00 00 00 26 00 00 00
65 00 00 00 2e 00 00 00 d9 00 00 00 49 00 00 00
57 00 00 00 5d 00 00 00 ac 00 00 00 a2 00 00 00
b0 00 00 00 0d 00 00 00 f6 00 00 00 c1 00 00 00
ee 00 00 00 fb 00 00 00 55 00 00 00 6f 00 00 00
a7 00 00 00 dc 00 00 00 75 00 00 00 0e 00 00 00
64 00 00 00 14 00 00 00 df 00 00 00 95 00 00 00
cf 00 00 00 3e 00 00 00 f2 00 00 00 f5 00 00 00
41 00 00 00 d3 00 00 00 e2 00 00 00 b7 00 00 00
80 00 00 00 3b 00 00 00 27 00 00 00 7b 00 00 00
5e 00 00 00 e1 00 00 00 2f 00 00 00 5a 00 00 00
70 00 00 00 11 00 00 00""")
enc = bytes.fromhex("""
07 56 e5 58 71 89 9a ca f0 67 03 2d 49 fb 6e 86
c2 f7 48 ca 3c 43 db 8e 04 2a 56 4a 97 33 a1 a2
07 83 f0 89 19 13 77 b4 9f 7d 7b 9c dd 8e fd ad
b5 e2 28 0e 06 af e5 e3 86 c3 08 ad e6 4c de 63
a3 5f 1e 96 34 7d 9d 19 f5 c8 84 7f 7b 62 2a 6b
c1 28 3b 6d 09 ef fc cb a0 90 9a 3e 66 a2 4e 06
90 2c 9d ae 3c 99 40 53 4c 69 63 e7 b9 a8 b3 87
a5 97 98 fe 1f 20 51 a7 ae 0d 00 ab 16 35 59 3d
08 1b 1c 92 e2 4f 1d 86 a5 6e 0a 14 45 4d 61 08
69 c3 12 a2 eb 50 13 93 22 e2 c4 10 ca 5f b2 0b
a2 30 c8 54 91 3a 37 fd d2 10 ab 5a f8 38 f3 d3
d5 85 58 de df c0 f4 17 4e f7 31 79 dd 41 2f b3
20 c7 ec 98 5e ae f7 a9 cb 27 13 72 fe ca 64 ff
43 93 80 3e 1e e5 99 bf 41 4b 9d 85 4e 0f 99 94
57 e1 63 d9 01 85 78 8a 06 fe 9d 41 32 74 55 83
b2 85 e9 9f c6 2c 4b 62 8f bf 7d 57 c8 76 3b 31
5e 87 60 89 35 41 c1 52 6c d0 0b 7d ca 60 5d 82
19 b0 96 5e 16 e7 9b 2f 37 5f c9 c5 f3 20 c3 45
cb 47 a1 cc 79 e5 b6 fb d4 55 db c1 35 9b 8b fa
38 d5 b2 b5 e0 4f 4d 6c 4f 8c 0c 42 bc 8e b3 78
48 e4 87 8e 34 a3 1d 01 53 98 71 fa 8f 2f e3 7a
6b b9 1b b6 7e 34 7f c8 c4 6c ab 45 4d 81 ef ee
c3 d9 db 13 5b 63 90 fc 34 18 81 bc d1 18 48 bb
7c 24 5b 56 2b 35 6b d7 f9 d3 d5 2b e2 24 d8 50
f1 ec d5 e6 29 55 66 f2 f7 28 20 7d f3 47 40 03
11 4a 47 a5 b4 74 15 35 d0 f0 e5 4c 04 b5 59 fe
fc 45 9d 3a a1 3f 1a a7 a8 51 e5 65 f1 56 ee de
fc c4 87 f5 fa 79 31 07 0a 3f 41 28 d1 59 17 4d
02 e4 5a 22 3a bc d2 cd 80 bc 2a 49 f0 7f 97 a1
90 59 01 8d 25 43 d8 00 ea d8 4f e2 4e 2b 06 fd
7e 16 a9 92 c4 fd b5 6a 82 06 18 0c 0a b7 b8 29
8f 87 63 65 25 b9 7a d0 6e 30 3c f2 f7 c2 30 86
""")
flag = [z3.BitVec(f"f{i}", 8) for i in range(0x200)]
M = [int.from_bytes(map3[x:x+4], "little") for x in range(0, 0x408, 4)]
mem = [flag[0]] * (0x200)
for i in range(0, (2 * 0x20) * 8, 8):
x = z3.Concat(*(flag[i + j] for j in range(8)[::-1]))
y = x ^ z3.LShR(x, 0xc)
for j in range(8):
mem[i + j] = z3.Extract(8*j+7, 8*j, y)
out = [0] * 0x200
# --- function 1400010e0
u4 = M[0]
u7 = M[1]
p5 = 2
p9 = 2
for i in range(0x20):
u3 = u4 + 1 & 0xff
u1 = M[u3 + 2]
u8 = u1 + u7 & 0xff
u2 = M[u8 + 2]
M[u3 + 2] = u2
M[u8 + 2] = u1
out[p9 - 2] = (M[ (u2 + u1 & 0xff) + 2 ]&0xff) ^ mem[p9 + -2]
for k in range(15):
u3 = (u3 + 1) & 0xff
u1 = M[u3 + 2]
u8 = u8 + u1 & 0xff
u2 = M[u8 + 2]
M[u3 + 2] = u2
M[u8 + 2] = u1
out[p5 - 1 + k] = (M[ (u2 + u1 & 0xff) + 2 ]&0xff) ^ mem[p9 + -1 + k]
u4 = u3
u7 = u8
p5 += 0x10
p9 += 0x10
M[1] = u8
M[0] = u3
# --- function 1400010e0 [end]
for i in range(0, (2 * 0x20) * 8, 8):
x = z3.Concat(*(out[i + j] for j in range(8)[::-1]))
y = x ^ z3.LShR(x, 0xc)
for j in range(8):
mem[i + j] = z3.Extract(8*j+7, 8*j, y)
# memcmp
for c, d in zip(mem, enc):
s.add(c == d)
assert s.check()
m = s.model()
print("".join(f"{m.eval(c).as_long():c}" for c in flag))
```
## Flag
```
TSGCTF{y0u_w0uld_und3r57and_h0w_70_d3cryp7_arc4_and_h0w_70_d3cryp7_7h3_l3ak3d_5af3_l1nk1ng_p01n73r}
```
