CTF逆向 |
您所在的位置：网站首页 › ctf逆向checkin › CTF逆向 |
CTF逆向
|
查看文件内容  使用ida7.7版本打开，发现是go编写的程序。注意，ida在7.6版本以后才开始支持go的反编译，建议安装最新版ida。这之前只能是通过idago的插件实现。 新版本下载 CTF逆向-常用的逆向工具 提取码：pnbt进入后找到main_main函数的位置  发现是一堆对输入值的判断，使用z3的python库对其进行约束求解即可  为了方便看数组和变量的关系，可以按n键将其命名成和数组一样的名字以避免混淆。要注意v_multi是v_17 + v_11 - v_5 - v_18，v_18_minus_17是v_18 - v_17，在后续添加约束求解的时候要记得加括号，或者是直接将其变量整体添加一个约束，然后一起加入到条件中去。 if ( v_8 + 4 == v_1 && (v_17 = v2[17], v_11 = v2[11], 125 - v_17 + 40 == v_11) && (v_18 = v2[18], v_multi = v_17 + v_11 - v_5 - v_18, v_18_minus_17 = v_18 - v_17, v_multi == v_18_minus_17) && (v_6_minus_17 = v_6 - v_17, *v2 == v_18_minus_17 * (v_6_minus_17 >> 1) + 110) && (v_10 = v2[10], v_13 + 1 == v_10) && v_6_minus_17 + 2 * v_6_minus_17 + 4 * (v_4 - v_7) == v_10 && v2[20] - v_1 == 2 * v_18_minus_17 && (v_5 ^ 110) == 29 && v_6_minus_17 == 4 * v_18_minus_17 && v2[6] == v_14 ) { main_win(); v3 = v20; }最后得到解密的z3脚本 import z3 s = z3.Solver() v2 = [z3.Int(x) for x in range(23)] v2[2] = ord('t') v2[9] = ord('c') v2[16] = ord('n') v2[21] = ord('z') v2[22] = ord('}') v2[5] = ord('s') v2[3] = 18 ^ ord('t') v2[1] = ord('c') v2[7] = ord('d') v2[19] = ord('z') s.add(v2[13] == v2[12]) s.add(v2[14] + v2[6] == 104) s.add(v2[4] == 123) s.add(v2[8] == v2[15]) s.add(v2[8] + 4 == v2[1]) s.add(125 - v2[17] + 40 == v2[11]) s.add(v2[17] + v2[11] - v2[5] - v2[18] == (v2[18] - v2[17])) s.add(v2[0] == (v2[18] - v2[17]) * ((v2[6] - v2[17]) / 2) + 110) s.add(v2[13] + 1 == v2[10]) s.add(v2[6] - v2[17] + 2 * (v2[6] - v2[17]) + 4 * (v2[4] - v2[7]) == v2[10]) s.add(v2[20] - v2[1] == 2 * (v2[18] - v2[17])) s.add((v2[5] ^ 110) == 29) s.add(v2[6] - v2[17] == 4 * (v2[18] - v2[17])) s.add(v2[6] == v2[14]) r = s.check() print(r) if repr(r) == 'sat': result = s.model() for k in result: index = int(str(k).replace('k!', '')) v2[index] = result[k].as_long() print(v2) print(''.join([chr(x) for x in v2])) # pctf{s4d_chugg4_n01zez}运行得到flag pctf{s4d_chugg4_n01zez} |
【本文地址】