원글 페이지 : 바로가기
어제 (2024년 5월 27일) Dreamhack Invitational에서 대회를 치루었고, 생각했던 것보다 낮은 순위를 기록했다.. 19위에 랭크되었고, 대회 15문제 중 1문제밖에 풀지 못했다. 리버싱만 다 풀자는 마인드로 참여했는데 그게 잘 안 되었다.. ㅠㅠ 무엇이 문제였는가? 우선 1번 문제는 큰 문제는 아니였다. 1번 문제를 순삭하고 좋은 시작을 알렸다. solve.py # Use ‘IDA Decompiled results’ to parse the instructions
# use sweeping to parse strings
def parse1(s: str):
instructions = s.split(‘\n’)
m = []
elasped = 0
for inst in instructions:
# Case 1. Sleep: Add seconds to all
if ‘sleep’ in inst:
if ‘seconds’ in inst:
continue
try:
val = inst.split(‘(‘)[1].split(‘u)’)[0]
val = int(val, 16)
except ValueError:
val = inst.split(‘(‘)[1].split(‘)’)[0]
val = int(val, 16)
#print(inst, val)
elasped += val
# Case 2. Trylock: it means it’ll use.
if ‘pthread_mutex_trylock’ in inst:
val = inst.split(‘(‘)[2].split(‘)’)[0]
#print(inst, val)
m.append((‘start’, val, elasped))
# Case 3. Unlock: it means it’ll end.
if ‘pthread_mutex_unlock’ in inst:
val = inst.split(‘(‘)[1].split(‘)’)[0]
#print(inst, val)
m.append((‘end’, val, elasped))
return m
l = []
for i in range(64):
fname = str(i) + “.txt”
with open(fname, ‘r’) as f:
l.append(parse1(f.read()))
# 1. The range should be all distinct. Else it’ll cause boom
# 2.
from z3 import *
# Make sure we double check the list to verify it is good
S = set()
eqs = {}
for i in l:
for j in i:
S.add(j[1])
for f in S:
eqs[f] = []
#print(eqs)
values = [ Int(f”x_{i}”) for i in range(64) ]
s = Solver()
for i in values:
s.add(0 <= i)
s.add(i < 16)
for i, c in enumerate(l):
# i is the index of our char (flag)
d = values[i]
# let us make these to equations, and push back to the equations
qs = {}
for op, what, elasped in c:
#print(op, what, elasped, qs)
if op == 'start':
qs[what] = elasped
else:
for i in range(qs[what], elasped + 1):
eqs[what].append(d + i)
qs.pop(what)
# the operations' range SHOULD be distinct; excluding both endpoints
for k in eqs.keys():
v = eqs[k]
for i in range(len(v)):
for j in range(i + 1, len(v)):
s.add(v[i] != v[j])
s.check()
m = s.model()
alpha = "0123456789abcdef"
for i in range(64):
print(alpha[m[Int(f"x_{i}")].as_long()], end='')
# Last check
s.add(Int(f"x_{0}") != m[Int(f"x_{0}")].as_long())
assert(s.check() == unsat) z3을 사용하여 파싱하면 풀리는 문제였고, 그다지 어렵지 않았던 것 같다. 하지만 문제는 2번 문제였다. 2번 문제만 8시간 잡다가 대회 자체를 날려먹었다. 진짜 하나도 모르겠어서 대회 끝나고 쌉고트 ks님께 물어보니 input을 256비트 정수로 치환하고 미리 정해진 값 A랑 곱셈을 한 결과에 대해서 2^256-1로 나눈 나머지가 1이 되게 하는, 한 마디로 모듈러 역원을 구하는 문제였다고... 하지만 이게 이렇게만 있다면 대회 중 풀 수 있었을지도 모른다. 하지만 어려운 점 두 가지는 Modulus (2^256-1)를 발견하기까지 발상이 정말 어렵다는 점과 index가 순환하는데 이것을 무시해도 된다는 것이였다. (증명: 2^(256+k) = 2^k (mod 2^256-1)) 정말 암호학같은 리버싱 문제였다..ㅠㅠ solve.py (from ks) num = 0
for i in range(0x100):
num |= table_a[i] << i
mod = (1 << 256) - 1
ans = pow(num, -1, mod)
print(hex(ans)[2:][::-1]) 전에 말했듯 2번 문제만 잡느라 다른 문제를 거들떠 보지도 않았다. 2번 말고 3번을 잡았다면 풀 수 있었을지도... 모르겠다! 3번 문제를 대회 끝나고 다음 날 (5월 28일) 6시간 정도 잡아서 풀었다. 대충 암호화 루틴 똑같은 것 20개 복호화하면 풀리는 문제였다. 2번 문제 말고 진작 3번 문제 볼걸... origin = [
0x16, 0xf0, 0x67, 0xa0, 0x74, 0x35, 0xe9, 0xad, 0x93, 0x8b, 0x60, 0x97, 0xe6, 0x6b, 0x18, 0x44
]
z_box = bytes.fromhex('FF 0E 8F 3B E9 0D 39 25 43 96 78 9C DE 1B 64 17 D2 9D 99 40 9F 73 A0 B0 EB 8C D3 07 24 11 38 56 CB EE 85 F5 1F 0E 84 89 8E AF A4 F1 13 26 AE C2 59 92 DF FF 10 F5 E0 D6 63 42 EC 63 BC AC D7 B9 53 40 1F 28 BE 33 93 DA 0C 6F C2 3F 17 44 0F 41 6E 0C 0C 15 4F 6D 14 C7 4B AA B9 98 C2 17 DA 5C 07 FA 65 14 D7 77 42 86 CD 16 5B 43 2B 82 12 88 6D CF AA 81 CD 38 19 6E BD A0 24 53 43 B9 09 BD 22 E9 FC 78 2C FE 09 29 F5 87 54 F6 5B 72 BE 69 25 9C FB B9 53 82 EB CE E1 C3 55 6B 3D 48 36 F5 85 6E DB A1 18 C0 25 96 42 80 CE 49 E2 6F 60 67 59 EA DF B0 43 1E CC 86 C9 F5 A6 2F 29 A6 B3 07 3C BA 40 BB 61 A2 EB 69 D3 21 8F 81 BC 55 77 CA B5 22 31 02 6D 05 2C 6F 84 F4 9B 57 30 6F 52 55 4D 5C EF 84 17 CF 54 C4 80 E4 D7 E0 E3 B1 C1 39 CC 9F A9 CB 49 20 BF 5E 52 E6 54 11 A2 7D AE E1 F9 FF 08 21 9E A8 16 D1 36 D8 51 A2 75 D2 51 5C 47 D2 22 1C 5C 1B 94 E8 49 10 74 03 C5 97 09 80 00 09 82 2C 40 D5 2F F1 2D 9B BB C8 7B 9E D6 92 22 24 4D 23 44 99 68 C9 5F 68 54 85 4C B1 F7 8F')
t_box = [
0x58D95FEE, 0x6C0E5938, 0x915DF01F, 0x4958472D, 0x8433197A,
0xF8C2D76D, 0x823A9DCC, 0x343A2EBB, 0x45D663D5, 0x2DEE8F26,
0x605A7989, 0x12436086, 0x3C49AC62, 0xC68441BD, 0xF3517A32,
0x3A9A440C, 0x5611D155, 0x26F0789D, 0xEBCCE2F5, 0xE9760B4C
]
s_box = list(bytes.fromhex('12 DE 65 32 18 72 D6 CD 83 D7 99 80 63 E4 A2 CE 23 9B CC DF 24 3B E2 7F 2D 4C 06 37 DD 52 92 5A 1A 17 68 14 2B 10 A4 3E 6B 96 7B 07 30 16 C8 A5 B8 3C 62 8E 3D E7 D8 08 95 64 CB 9D E8 5C 15 66 D2 86 01 56 D4 1C B7 9E AC 54 6E 28 36 8C 73 22 0E C5 C1 FF 3A EB 29 2F AE 0F F7 BA 98 93 B2 F8 55 E9 F5 A8 02 77 EA 7A FA 00 44 D5 1B 5F C0 A1 EC 67 58 DA DC A7 C3 B5 1E 03 42 90 71 45 E3 2A F0 CF 7C B6 94 C4 D0 E6 05 F1 89 82 D9 C7 20 9A 4B 1F 5E 39 1D 88 74 8D EF 2C 41 FC 79 DB 6D 35 B0 F3 48 6F 34 B9 57 6C 4E 51 3F 2E 09 CA 47 6A 8A 5D A0 40 D3 FB 25 E0 8B F2 61 4D C2 70 8F AA 46 B1 D1 E5 76 38 75 4A 26 11 C9 4F E1 97 B3 43 27 5B A3 AF 19 85 BD 60 59 0A 13 BC A9 91 F6 EE 84 53 F4 0C AD BF 04 21 81 BE 78 C6 7D 87 A6 ED 9F 9C 49 F9 0B 33 69 B4 FE 0D 7E 50 AB 31 FD BB'))
f_box = bytes.fromhex('69 02 70 24 8F A9 8A D6 57 41 06 F1 70 59 A6 21 1D 5B 06 BD 46 85 A0 CF FB F9 EB 00 34 F1 EA CC 43 93 A6 5D BE 53 90 90 10 19 99 39 6B 2D D2 32 F8 16 A2 25 7D 13 D2 B4 EC D0 0A 6C 60 0C F8 2E A6 59 86 8B 2D 89 E7 7D 63 37 EC 68 59 7D D8 4C 5A C3 34 E7 85 90 BD CF 92 13 2D 7D EB 1B BB 39 71 D7 91 53 2C 68 4C 6A 72 8F E4 05 A3 62 DF CE DE 8F AA 94 45 6F 5D 6A B0 22 74 24 E1 56 E8 AE 9E 46 C7 54 45 24 3B 69 59 D2 15 FD BC 3F 67 5D 0B C4 2B 01 3F B7 46 45 03 20 D0 96 50 FD BE 2A 4F A5 E0 F3 A0 F5 D6 56 BB 1E 41 83 D8 CA B8 54 D2 3C 6B 9E E7 D1 6B 4B F5 AA DB 9B 2D F8 99 5C CA 9E 09 D9 21 A9 B5 EA 79 B6 D7 2C 51 90 99 8A C5 06 93 84 FB DB 29 A5 86 47 E1 1A 01 E4 49 23 C8 A5 2C 32 49 A4 F4 FE F9 2C 5B 8E AB 5F 69 FC 92 E1 03 40 B1 D9 92 EC 03 36 F7 B2 B2 EC 8F 20 F3 26 2D 18 27 18 1D D6 24 BF 3E 07 3B 7C CF F8 E1 2B C0 E8 AD 2A F3 54 BB 18 B4 12 50 70 1C 45 BA E8 24 70 16 72 38 4C A5 54 1D 88 0B D4 E0 7A 80 CA 39 6D 2B 25 CF 6F B2 51 2B D4 38 9F 7F 10')
assert(len(z_box) == 320)
assert(len(t_box) == 20)
assert(len(s_box) == 256)
assert(len(f_box) == 320)
import numpy as np
from sympy import Matrix
def l2sm(l):
ret = [[] for _ in range(4)]
for i in range(4):
for j in range(4):
ret[i].append(l[i * 4 + j])
return np.array(ret)
def sm2l(sm):
ret = []
for i in range(4):
for j in range(4):
ret.append(sm[i][j])
return ret
from ctypes import CDLL
libc = CDLL('libc.so.6')
FIELD = 256
def decode_z(enc, box):
assert(len(box) == 16)
assert(len(enc) == 16)
c = l2sm(box) % FIELD # c
a = l2sm(enc) % FIELD # a
print("A:",a, "C:",c,sep='\n')
mat_c = Matrix(c)
inv_mat_c = mat_c.inv_mod(FIELD)
inv_c = np.array(inv_mat_c).astype(int)
b_mod = np.dot(a, inv_c) % FIELD
return sm2l(b_mod)
def decode_t(enc, box):
assert(len(enc) == 16)
libc.srand(box)
rands = []
counter = 0
while True:
r1 = libc.rand()
if r1 <= counter:
break
rands.append(r1) # Notice we just ignored last random value.
counter += 1
r2 = libc.rand()
r3 = libc.rand()
rands.append(r2)
rands.append(r3)
print(len(rands))
assert(len(rands) % 3 == 0)
dec = [] + enc
for i in range(len(rands) - 1, -1, -3):
r3 = rands[i] % 16
r2 = rands[i - 1] % 16
tmp = dec[r3]
dec[r3] = dec[r2]
dec[r2] = tmp
return dec
def decode_s(enc):
b = [] + enc
a = [ 0 for _ in range(16)]
assert(len(a) == len(b))
for i in range(256, -1, -1):
for j in range(16):
if i % 2 == 0:
a[(i + j) % 16] = s_box.index(b[j])
else:
b[(i + j) % 16] = s_box.index(a[j])
return a
def decode_f(enc, box):
assert(len(enc) == 16)
assert(len(box) == 16)
dec = []
for i in range(16):
dec.append(enc[i] ^ box[i])
return dec
for i in range(19, -1, -1):
origin = decode_z(origin, z_box[16*i:16*(i+1)])
print(origin)
origin = decode_t(origin, t_box[i])
print(origin)
origin = decode_s(origin)
print(origin)
origin = decode_f(origin, f_box[16*i:16*(i+1)])
print(origin)
print(bytes(origin)) Conclusion 앞으로 대회에 이런 수학적 사고력을 심히 요구하는 리버싱 문제가 많이 나올 것 같고 이를 대비하는 자세가 필요할 것 같다. 솔직히 나로서는 Windows 테크닉 문제가 하나쯤 나왔으면 하고 내심 기대하고 있다. (LINE CTF 2024 때처럼)