BUUCTF - RE - [ACTF新生赛2020]Universe_final_answer（buuctf面具下的flag）

BUUCTF - RE - [ACTF新生赛2020]Universe_final_answer（buuctf面具下的flag）

老规矩，先拉进IDA

逻辑很直接，主要是check函数，check2函数的结果似乎是用于输出flag的，那么先看check函数

简单、直接、粗暴，对输入进行检测，如果能通过一连串的运算就说明flag正确，如果爆破的话，不知要爆破到何年何月，这时候就是z3大展身手的时候了，安装：

pip2 install z3-solver

先将运算从IDA中取出洗干净待用：

-85 * num[8] + 58 * num[7] + 97 * num[5] + num[6] + -45 * num[4] + 84 * num[3] + 95 * num[1] - 20 * num[0] + 12 * num[2] == 12613 30 * num[9] + -70 * num[8] + -122 * num[5] + -81 * num[6] + -66 * num[4] + -115 * num[3] + -41 * num[2] + -86 * num[0] - 15 * num[1] - 30 * num[7] == -54400 -103 * num[9] + 120 * num[7] + 108 * num[6] + 48 * num[3] + -89 * num[2] + 78 * num[0] - 41 * num[1] + 31 * num[4] - (num[5] << 6) - 120 * num[8] == -10283 71 * num[5] + (num[6] << 7) + 99 * num[4] + -111 * num[2] + 85 * num[0] + 79 * num[1] - 30 * num[3] - 119 * num[7] + 48 * num[8] - 16 * num[9] == 22855 5 * num[9] + 23 * num[8] + 122 * num[7] + -19 * num[5] + 99 * num[6] + -117 * num[4] + -69 * num[2] + 22 * num[0] - 98 * num[1] + 10 * num[3] == -2944 -54 * num[9] + -23 * num[7] + -82 * num[2] + -85 * num[1] + 124 * num[0] - 11 * num[3] - 8 * num[4] - 60 * num[6] + 95 * num[5] + 100 * num[8] == -2222 -83 * num[9] + -111 * num[6] + -57 * num[1] + 41 * num[0] + 73 * num[2] - 18 * num[3] + 26 * num[4] + 16 * num[5] + 77 * num[7] - 63 * num[8] == -13258 81 * num[9] + -48 * num[8] + 66 * num[7] + -104 * num[5] + -121 * num[6] + 95 * num[4] + 85 * num[3] + 60 * num[2] + -85 * num[1] + 80 * num[0] == -1559 101 * num[9] + -85 * num[8] + 7 * num[5] + 117 * num[6] + -83 * num[4] + -101 * num[3] + 90 * num[2] + -28 * num[0] + 18 * num[1] - num[7] == 6308 99 * num[9] + -28 * num[8] + 5 * num[7] + 93 * num[5] + -18 * num[6] + -127 * num[4] + 6 * num[3] + -9 * num[2] + -93 * num[0] + 58 * num[1] == -1697

写脚本：

s='''-85 * num[8] + 58 * num[7] + 97 * num[5] + num[6] + -45 * num[4] + 84 * num[3] + 95 * num[1] - 20 * num[0] + 12 * num[2] == 12613 30 * num[9] + -70 * num[8] + -122 * num[5] + -81 * num[6] + -66 * num[4] + -115 * num[3] + -41 * num[2] + -86 * num[0] - 15 * num[1] - 30 * num[7] == -54400 -103 * num[9] + 120 * num[7] + 108 * num[6] + 48 * num[3] + -89 * num[2] + 78 * num[0] - 41 * num[1] + 31 * num[4] - (num[5] << 6) - 120 * num[8] == -10283 71 * num[5] + (num[6] << 7) + 99 * num[4] + -111 * num[2] + 85 * num[0] + 79 * num[1] - 30 * num[3] - 119 * num[7] + 48 * num[8] - 16 * num[9] == 22855 5 * num[9] + 23 * num[8] + 122 * num[7] + -19 * num[5] + 99 * num[6] + -117 * num[4] + -69 * num[2] + 22 * num[0] - 98 * num[1] + 10 * num[3] == -2944 -54 * num[9] + -23 * num[7] + -82 * num[2] + -85 * num[1] + 124 * num[0] - 11 * num[3] - 8 * num[4] - 60 * num[6] + 95 * num[5] + 100 * num[8] == -2222 -83 * num[9] + -111 * num[6] + -57 * num[1] + 41 * num[0] + 73 * num[2] - 18 * num[3] + 26 * num[4] + 16 * num[5] + 77 * num[7] - 63 * num[8] == -13258 81 * num[9] + -48 * num[8] + 66 * num[7] + -104 * num[5] + -121 * num[6] + 95 * num[4] + 85 * num[3] + 60 * num[2] + -85 * num[1] + 80 * num[0] == -1559 101 * num[9] + -85 * num[8] + 7 * num[5] + 117 * num[6] + -83 * num[4] + -101 * num[3] + 90 * num[2] + -28 * num[0] + 18 * num[1] - num[7] == 6308 99 * num[9] + -28 * num[8] + 5 * num[7] + 93 * num[5] + -18 * num[6] + -127 * num[4] + 6 * num[3] + -9 * num[2] + -93 * num[0] + 58 * num[1] == -1697'''.split('\n') from z3 import * num=[BitVec('num[%d]'%i,8) for i in range(10)] solver=Solver() for i in num:     solver.add(i<=126)     solver.add(32<=i) for i in s:     exec('solver.add(%s)'%i) solver.check() print solver.model()

还需要注意的是，伪代码中[0]和[1]，[5]和[6]是相反的，如果代码是基于伪代码的话，就需要翻转一下

然后将得到的字符串输入到程序中就得到flag了

版权声明：本文内容由网络用户投稿，版权归原作者所有，本站不拥有其著作权，亦不承担相应法律责任。如果您发现本站中有涉嫌抄袭或描述失实的内容，请联系我们jiasou666@gmail.com 处理，核实后本网站将在24小时内删除侵权内容。