Tags: reverse-engineering
Rating:
This challenge lives up to its description - 200 bytes of data are read in, following which each byte is run through a separate function. However, the functions are very similar and are luckily arranged in the correct order in the binary. Running the binary through ghidra and dumping the result as C, the result is
...
uint f122323(char param_1)
{
uint uVar1;
uVar1 = (int)(param_1 >> 4) + ((int)param_1 & 0xfU) * 0x10;
return uVar1 & 0xffffff00 | (uint)(uVar1 == 0x46);
}
uint f7093176(char param_1)
{
uint uVar1;
uVar1 = (int)(param_1 >> 4) + ((int)param_1 & 0xfU) * 0x10;
return uVar1 & 0xffffff00 | (uint)(uVar1 == 0x16);
}
...
The returned value needs to be nonzero, so the second condition comparing uVar1 should be true. The values being compared to are the only values that differ across the functions and can be extracted with a regex:
uVar1 == (?:0x)?([a-f0-9]{1,2})
(Ghidra dumps smaller values in decimal.) Then all that's left to do is to get back the parameter values, which z3 can easily solve (the previously extracted hexadecimal values saved in all):
from z3 import *
def do_solve(x):
sol = z3.Solver()
v = z3.BitVec("v", 32)
sol.add(v > 0)
sol.add(v < 256)
v2 = (v >> 4) + (v & 0xf) * 0x10
sol.add(v2 == x)
sol.check()
s = sol.model()
return s[v].as_long()
j = ""
with open("all") as f:
for l in f:
if l.strip() != "":
v = int(l.strip(), 16)
s = do_solve(v)
print(v, s, chr(s))
j += chr(s)
print(j)
# darkCON{4r3_y0u_r34lly_th1nk1n9_th4t_y0u_c4n_try_th15_m4nu4lly???_Ok_I_th1nk_y0u_b3tt3r_us3_s0m3_aut0m4t3d_t00ls_l1k3_4n9r_0r_Z3_t0_m4k3_y0ur_l1f3_much_e4s13r.C0ngr4ts_f0r_s0lv1in9_th3_e4sy_ch4ll3ng3}
