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.
Possible 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
After 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
c
For 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
Okay 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
Then 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()
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 :> .
