Reverse Engineering
1125899906842622 (18 solves)
Description
I found this credit card on the floor!
a = int(input())
t = a
b = 1
c = 211403263193325564935177732039311880968900585239198162576891024013795244278301418972476576250867590357558453818398439943850378531849394935408437463406454857158521417008852225672729172355559636113821448436305733721716196982836937454125646725644730318942728101471045037112450682284520951847177283496341601551774254483030077823813188507483073118602703254303097147462068515767717772884466792302813549230305888885204253788392922886375194682180491793001343169832953298914716055094436911057598304954503449174775345984866214515917257380264516918145147739699677733412795896932349404893017733701969358911638491238857741665750286105099248045902976635536517481599121390996091651261500380029994399838070532595869706503571976725974716799639715490513609494565268488194
verified = False
while 1:
if b == 4:
verified = True
break
d = 2 + (1125899906842622 if a&2 else 0)
if a&1:
b //= d
else:
b *= d
b += (b&c)*(1125899906842622)
a //= 4
if verified:
t %= (2**300)
t ^= 1565959740202953194497459354306763253658344353764229118098024096752495734667310309613713367
print(t)Solution
From the source code we can see that there is 4 possibility of our input since our input processed each 2 bit.
xx11 -> (b // 1125899906842624) + ((b // 1125899906842624)&c)*1125899906842622
xx10 -> (b * 1125899906842624) + ((b * 1125899906842624)&c)*1125899906842622
xx01 -> (b // 2) + ((b // 2)&c)*1125899906842622
xx00 -> (b * 2) + ((b * 2)&c)*1125899906842622Possible first 2 bits should be 10 and 00 cause if we use 01 and 11 it should produce b == 0 . After struggling to find the base case or constraint for recursive function i try to find the relation of b and c variable. We can see that the first possible value are 10 and 00 , it looks like an entry corner to a maze since we can go right and down if we start from top left corner. Since c is square number (bit_length == 2500), so we try to use this value as the map. For the c value, since it uses and operator , the bit processed should be from the last bit so we need to reverse the binary to start the maze from initial position (0, 0). Last step, just implement Depth First Search (DFS) algorithm to find the correct path. Here is my implementation on python.
from Crypto.Util.number import *
def check(coor):
if(mapp[coor[0]][coor[1]] == 1):
return False
if(coor[0] < 0 or coor[0] > 49 or coor[1] < 0 or coor[1] > 49):
return False
return True
def parse(path):
res = ""
for i in range(1,len(path)):
tmp = (path[i][0] - path[i-1][0], path[i][1] - path[i-1][1] )
if(tmp == (1, 0)):
res = "10" + res
elif(tmp == (0, 1)):
res = "00" + res
elif(tmp == (0, -1)):
res = "01" + res
elif(tmp == (-1, 0)):
res = "11" + res
else:
print("???")
return int(res,2)
def dfs(coor):
if(coor == finish):
t = parse(visited)
t %= (2**300)
t ^= 1565959740202953194497459354306763253658344353764229118098024096752495734667310309613713367
print(long_to_bytes(t))
exit()
up = (coor[0], coor[1] - 1)
down = (coor[0], coor[1] + 1)
right = (coor[0] + 1, coor[1])
left = (coor[0] - 1, coor[1])
if(check(up) and up not in visited):
visited.append(up)
if(dfs(up)):
return True
visited.pop()
if(check(down) and down not in visited):
visited.append(down)
if(dfs(down)):
return True
visited.pop()
if(check(right) and right not in visited):
visited.append(right)
if(dfs(right)):
return True
visited.pop()
if(check(left) and left not in visited):
visited.append(left)
if(dfs(left)):
return True
visited.pop()
return False
c = 211403263193325564935177732039311880968900585239198162576891024013795244278301418972476576250867590357558453818398439943850378531849394935408437463406454857158521417008852225672729172355559636113821448436305733721716196982836937454125646725644730318942728101471045037112450682284520951847177283496341601551774254483030077823813188507483073118602703254303097147462068515767717772884466792302813549230305888885204253788392922886375194682180491793001343169832953298914716055094436911057598304954503449174775345984866214515917257380264516918145147739699677733412795896932349404893017733701969358911638491238857741665750286105099248045902976635536517481599121390996091651261500380029994399838070532595869706503571976725974716799639715490513609494565268488194
mapp = []
a = bin(c)[2:][::-1]
assert(len(a) == 2500)
for i in range(0,len(a),50):
tmp = []
for j in range(50):
tmp.append(int(a[i+j]))
mapp.append(tmp)
visited = [(0,0)]
coor = (0,0)
finish = (49,49)
mapp[finish[0]][finish[1]] = 0
dfs(coor)
Flag : flag{l4byr1nth_9abe79d712e6dd52c4597}
re-cursed (4 solves)
Description
Scotland forever!
Solution
First step, we should extract the original elf executed in recursed binary. This should be done by set breakpoint on write function and dump the memory
dump binary memory result.bin 0x00007fffffbd5450 0x00007fffffbd5450+0x0000000000428f10After that we should facing the real cursed binary, compiled using ghc and of course it made using haskell. In this case we can't use https://github.com/gereeter/hsdecomp or another modified hsdecomp. So my initial approach by enumerating what instruction that processed our input. It can be done by doing hardware breakpoint on our input.
From image above we can see that our input stored at 0x7fffffffe701. Next step is doing hardware breakpoint on that address by using command below
rwatch *0x7fffffffe701
After some enumeration i found that there is something like argument processing and we can skip that by setting up breakpoint on 0x4afbae
After hitting breakpoint, search value for our argument. In this case i used RYUK12345 as argument
There are some value found on memory, we can enumerate 1 by 1. In this challenge, i found that 0x507b70 used for next process. The next step is changing the hardware breakpoint each the value moved or processed by the instruction, here is for example
Do the same process until you find something interesting. In this case we found interesting function that process our input at first time, it is ghczmbignum_GHCziNumziInteger_integerXor_info .
Take a look on decompiler it contains so much code just for "xor" operation. But again we can validate which instruction process our value. It is relative simple since the code that doing xor for different value only on line 159 or address 0x49FB98
The function name has pattern, so we can try set breakpoint on function that maybe process our input.
For example we can just do command like below
b *ghczmbignum_GHCziNumziInteger_integerAdd_info
cFor finding the exact instruction it is same, just debug and validate that there is your input processed by the instruction (if it is hard to find through decompiler). At the end i found the following address that processed our input
0x49fb98 -> ghczmbignum_GHCziNumziInteger_integerXor_info
0x499929 -> ghczmbignum_GHCziNumziInteger_integerAdd_info
0x49839b -> ghczmbignum_GHCziNumziInteger_integerSub_info
0x4978f0 -> ghczmbignum_GHCziNumziInteger_integerEqzh_infoOkay next we just need to create automation to get all value processed by those instruction. Here is the script i used for gdb automation
#!/usr/bin/python3
import string
data = []
class SolverEquation(gdb.Command):
def __init__ (self):
super (SolverEquation, self).__init__ ("solve-equation",gdb.COMMAND_OBSCURE)
def invoke (self, arg, from_tty):
global data
gdb.execute("del")
gdb.execute("start")
gdb.execute("b *0x49fb98")
gdb.execute("b *0x499929")
gdb.execute("b *0x49839b")
gdb.execute("b *0x4978f0")
# gdb.execute("r 0123456789abcdefghijklmnopq") # cmp1
# gdb.execute("r ABCDEFGHIJKLMNOPQRSTUVWXYZa") # cmp2
# gdb.execute("r aaaaaaaaaaaaaaaaaaaaaaaaaaa") # cmp3
# gdb.execute("r AAAAAAAAAAAAAAAAAAAAAAAAAAA") # cmp4
gdb.execute("r qponmlkjihgfedcba9876543210") # cmp5
arch = gdb.selected_frame().architecture()
while True:
try:
current_pc = addr2num(gdb.selected_frame().read_register("pc"))
disa = arch.disassemble(current_pc)[0]
if("xor" in disa["asm"]):
rax = addr2num(gdb.selected_frame().read_register("rax"))&0xff
rbx = addr2num(gdb.selected_frame().read_register("rbx"))&0xff
fmt = f"{rax} ^ {rbx} = {rax^rbx}"
data.append(fmt)
elif("add" in disa["asm"]):
rax = parse(gdb.execute("x/bx $rax",to_string=True))[0]&0xff
rbx = addr2num(gdb.selected_frame().read_register("rbx"))&0xff
fmt = f"{rax} + {rbx} = {rax+rbx}"
data.append(fmt)
elif("sub" in disa["asm"]):
rbx = parse(gdb.execute("x/bx $rbx",to_string=True))[0]&0xff
rax = addr2num(gdb.selected_frame().read_register("rax"))&0xff
fmt = f"{rax} - {rbx} = {(rax-rbx)&0xff}"
data.append(fmt)
elif("cmp" in disa["asm"]):
rbx = parse(gdb.execute("x/bx $rbx+0x7",to_string=True))[0]&0xff
rax = addr2num(gdb.selected_frame().read_register("rax"))&0xff
fmt = f"{rax} == {rbx} = {(rax == rbx)}"
data.append(fmt)
else:
data.append("???")
gdb.execute("c")
except Exception as e:
for i in data:
print(i)
print(e)
break
def parse(f):
f = f.split("\n")
result = []
for i in f:
tmp = i.split("\t")
for j in range(1,len(tmp)):
result.append(int(tmp[j],16))
return result
def addr2num(addr):
try:
return int(addr) # Python 3
except:
return long(addr) # Python 2
SolverEquation()
Since there are many values are same, so i use different value as our input for 5 times to get 5 different output. Each output i saved it to file and named it as cmp{i} . Here is example for cmp5 file, output from input qponmlkjihgfedcba9876543210
113 ^ 57 = 72
112 ^ 72 = 56
111 ^ 56 = 87
110 ^ 87 = 57
109 ^ 57 = 84
108 ^ 84 = 56
107 ^ 56 = 83
106 ^ 83 = 57
105 ^ 57 = 80
104 ^ 80 = 56
103 ^ 56 = 95
102 ^ 95 = 57
101 ^ 57 = 92
100 ^ 92 = 56
99 ^ 56 = 91
98 ^ 91 = 57
97 ^ 57 = 88
57 ^ 88 = 97
56 ^ 97 = 89
55 ^ 89 = 110
54 ^ 110 = 88
53 ^ 88 = 109
52 ^ 109 = 89
51 ^ 89 = 106
50 ^ 106 = 88
49 ^ 88 = 105
48 ^ 105 = 89
87 - 24 = 63
63 ^ 43 = 20
5 + 20 = 25
22 - 25 = 253
3 + 72 = 75
75 ^ 43 = 96
5 + 96 = 101
78 - 101 = 233
253 ^ 233 = 20
56 ^ 43 = 19
5 + 19 = 24
29 - 24 = 5
20 ^ 5 = 17
56 - 24 = 32
32 ^ 43 = 11
5 + 11 = 16
37 - 16 = 21
17 ^ 21 = 4
3 + 57 = 60
60 ^ 43 = 23
5 + 23 = 28
24 - 28 = 252
4 ^ 252 = 248
84 ^ 43 = 127
5 + 127 = 132
106 - 132 = 230
248 ^ 230 = 30
80 - 24 = 56
56 ^ 43 = 19
5 + 19 = 24
5 - 24 = 237
30 ^ 237 = 243
3 + 83 = 86
86 ^ 43 = 125
5 + 125 = 130
105 - 130 = 231
243 ^ 231 = 20
57 ^ 43 = 18
5 + 18 = 23
14 - 23 = 247
20 ^ 247 = 227
57 - 24 = 33
33 ^ 43 = 10
5 + 10 = 15
0 - 35 = 221
221 - 15 = 206
227 ^ 206 = 45
3 + 56 = 59
59 ^ 43 = 16
5 + 16 = 21
6 - 21 = 241
45 ^ 241 = 220
95 ^ 43 = 116
5 + 116 = 121
127 + 5 = 132
132 - 121 = 11
220 ^ 11 = 215
91 - 24 = 67
67 ^ 43 = 104
5 + 104 = 109
83 - 109 = 230
215 ^ 230 = 49
3 + 92 = 95
95 ^ 43 = 116
5 + 116 = 121
75 - 121 = 210
49 ^ 210 = 227
56 ^ 43 = 19
5 + 19 = 24
56 - 24 = 32
227 ^ 32 = 195
97 - 24 = 73
73 ^ 43 = 98
5 + 98 = 103
41 - 103 = 194
195 ^ 194 = 1
3 + 57 = 60
60 ^ 43 = 23
5 + 23 = 28
19 - 28 = 247
1 ^ 247 = 246
88 ^ 43 = 115
5 + 115 = 120
106 - 120 = 242
246 ^ 242 = 4
88 - 24 = 64
64 ^ 43 = 107
5 + 107 = 112
122 - 112 = 10
4 ^ 10 = 14
3 + 89 = 92
92 ^ 43 = 119
5 + 119 = 124
105 - 124 = 237
14 ^ 237 = 227
110 ^ 43 = 69
5 + 69 = 74
7 - 74 = 189
227 ^ 189 = 94
106 - 24 = 82
82 ^ 43 = 121
5 + 121 = 126
51 - 126 = 181
94 ^ 181 = 235
3 + 109 = 112
112 ^ 43 = 91
5 + 91 = 96
61 - 96 = 221
235 ^ 221 = 54
89 ^ 43 = 114
5 + 114 = 119
92 - 119 = 229
54 ^ 229 = 211
89 - 24 = 65
65 ^ 43 = 106
5 + 106 = 111
124 - 111 = 13
211 ^ 13 = 222
3 + 88 = 91
91 ^ 43 = 112
5 + 112 = 117
91 - 117 = 230
222 ^ 230 = 56
105 ^ 43 = 66
5 + 66 = 71
39 - 71 = 224
56 ^ 224 = 216
216 == 0 = FalseThen i wrote a script to parse which value are constant and which value are variable. Also i write optimization to format it to equation format at the end.
def parse(a1):
tmp = a1.split(" ")
return tmp
def check_ret(a1, a2, res2, res3):
result = []
for i in range(len(res2)):
if((a1 == res2[i]) and (a2 == res3[i])):
result.append(i)
return result
def optimize(res, inp):
tmp = res[27:]
operator = ['+', '-', '^']
arr = []
opt = []
data = ''
init = True
for i in tmp:
# print(i) # debug
check = True
for j in inp:
if(j in i):
if(init and len(data) != 0):
opt.append(data)
init = False
data = ' '.join(i[:3])
check = False
break
if(check):
if("res" in i[0] and "res" in i[2] and "^" == i[1]):
opt.append(data)
continue
else:
tmp2 = []
for j in range(3):
if("res[" not in i[j]):
tmp2.append(i[j])
str_tmp2 = ' '.join(tmp2)
for j in operator:
if(tmp2[0] == j):
data = f"({data}) {str_tmp2}"
break
if(tmp2[1] == j):
data = f"{str_tmp2} ({data})"
break
return '\n'.join(opt)
def check(f, g):
res = []
res2 = []
res3 = []
cnt_var = 0
inp = [f"res[{i}]" for i in range(27)]
for ind in range(len(g)):
a1 = parse(f[ind])
a2 = parse(g[ind])
if(a1 == a2):
res.append(a1)
continue
tmp_res = []
for i in range(3):
if(a1[i] != a2[i]):
tmp_check = check_ret(a1[i], a2[i], res2, res3)
length = len(tmp_check)
if(length > 0):
if(length > 1):
val = '_'.join(map(str,tmp_check))
if(ind < 27):
inp.append(f"res[{val}]")
tmp_res.append(f"res[{val}]")
else:
tmp_res.append(f"res[{tmp_check[0]}]")
else:
tmp_res.append(f"var[{cnt_var}]")
cnt_var += 1
else:
tmp_res.append(a1[i])
tmp_res.append(a1[3])
tmp_res.append(f"res[{len(res2)}]")
res.append(tmp_res)
res2.append(a1[4])
res3.append(a2[4])
return optimize(res, inp)
def diff(f,g):
for i in range(min(len(f),len(g))):
a1 = parse(f[i])
a2 = parse(g[i])
if(a1[1] != a2[1]):
return i
return -1
files = [f"cmp{i}" for i in range(1,6)]
for i in range(len(files)):
for j in range(i+1,len(files)):
f = open(files[i],"r").read().split("\n")
g = open(files[j],"r").read().split("\n")
diff_index = diff(f, g)
if(diff_index != -1):
if(len(f) > len(g)):
f.pop(diff_index)
else:
g.pop(diff_index)
if(len(f) != len(g)):
print("ERR : ",files[i], files[j], diff_index)
else:
result = check(f,g)
out = open(f"{files[i]}_{files[j]}.out","w")
out.write(result)
out.close()Here is the example output for cmp1_cmp2.out file
22 - (5 + ((res[2] - 24) ^ 43))
78 - (5 + ((3 + res[0]) ^ 43))
29 - (5 + (res[1] ^ 43))
37 - (5 + ((res[5] - 24) ^ 43))
24 - (5 + ((3 + res[3]) ^ 43))
106 - (5 + (res[4] ^ 43))
5 - (5 + ((res[8] - 24) ^ 43))
105 - (5 + ((3 + res[6]) ^ 43))
14 - (5 + (res[7] ^ 43))
221 - (0 - 35 (5 + ((res[11] - 24) ^ 43)))
6 - (5 + ((3 + res[9]) ^ 43))
132 - (127 + 5 (5 + (res[10_14_18_22] ^ 43)))
83 - (5 + ((res[10_14_18_22] - 24) ^ 43))
75 - (5 + ((3 + res[12_16_20_24]) ^ 43))
56 - (5 + (res[13] ^ 43))
41 - (5 + ((res[17] - 24) ^ 43))
19 - (5 + ((3 + res[15]) ^ 43))
106 - (5 + (res[12_16_20_24] ^ 43))
122 - (5 + ((res[12_16_20_24] - 24) ^ 43))
105 - (5 + ((3 + res[10_14_18_22]) ^ 43))
7 - (5 + (res[19] ^ 43))
51 - (5 + ((res[23] - 24) ^ 43))
61 - (5 + ((3 + res[21]) ^ 43))
92 - (5 + (res[10_14_18_22] ^ 43))
124 - var[27] ((res[26] - 24) ^ 43)
91 - (5 + ((3 + res[12_16_20_24]) ^ 43))
39 - (5 + (res[25] ^ 43))Because there is still the same value, i fixed it manually by checking on each output with knowledge of the pattern used. Last, because i'm too lazy to reverse the process i just put the equation on z3 and got the flag also first blood :> .
from z3 import *
var = [BitVec("x{}".format(i), 8) for i in range(27)]
res = [0 for _ in range(27)]
res[0] = var[0] ^ 57
for i in range(1,27):
res[i] = var[i] ^ res[i-1]
s = Solver()
s.add(22 - (5 + ((res[2] - 24) ^ 43)) == 0)
s.add(78 - (5 + ((3 + res[0]) ^ 43)) == 0)
s.add(29 - (5 + (res[1] ^ 43))== 0)
s.add(37 - (5 + ((res[5] - 24) ^ 43)) == 0)
s.add(24 - (5 + ((3 + res[3]) ^ 43)) == 0)
s.add(106 - (5 + (res[4] ^ 43)) == 0)
s.add(5 - (5 + ((res[8] - 24) ^ 43)) == 0)
s.add(105 - (5 + ((3 + res[6]) ^ 43)) == 0)
s.add(14 - (5 + (res[7] ^ 43)) == 0)
s.add(221 - (5 + ((res[11] - 24) ^ 43)) == 0)
s.add(6 - (5 + ((3 + res[9]) ^ 43)) == 0)
s.add(132 - (5 + (res[10] ^ 43)) == 0)
s.add(83 - (5 + ((res[14] - 24) ^ 43)) == 0)
s.add(75 - (5 + ((3 + res[12]) ^ 43)) == 0)
s.add(56 - (5 + (res[13] ^ 43)) == 0)
s.add(41 - (5 + ((res[17] - 24) ^ 43)) == 0)
s.add(19 - (5 + ((3 + res[15]) ^ 43)) == 0)
s.add(106 - (5 + (res[16] ^ 43)) == 0)
s.add(122 - (5 + ((res[20] - 24) ^ 43)) == 0)
s.add(105 - (5 + ((3 + res[18]) ^ 43)) == 0)
s.add(7 - (5 + (res[19] ^ 43)) == 0)
s.add(51 - (5 + ((res[23] - 24) ^ 43)) == 0)
s.add(61 - (5 + ((3 + res[21]) ^ 43)) == 0)
s.add(92 - (5 + (res[22] ^ 43)) == 0)
s.add(124 - (5 + ((res[26] - 24) ^ 43)) == 0)
s.add(91 - (5 + ((3 + res[24]) ^ 43)) == 0)
s.add(39 - (5 + (res[25] ^ 43)) == 0)
print(s.check())
model = s.model()
flag = ""
for i in var:
flag += chr(model[i].as_long())
print(flag)
Flag : flag{monads_are_like_flags}
Last updated