老样子，先查壳，ELF64而且发现Upx壳. Tips:现在只会最基本的upx -d 脱壳，虽然现在不会OEP定律法，以后还是要面对的捏
丢kali里面进行脱壳即可
丢IDA继续分析
首先看字符串窗口发现有input your flag字样
跟进函数继续查看
整体函数的逻辑很简单，就是对多个变量输入字符串，然后通过sub_4009AE函数来判断是否正确或者错误，跟进sub_4009AE.
所以逻辑就是每个大数乘另一个大数都要为另一个大数，但是不管用C或者python写，都很反人类，人麻了。
不过之前做过新生赛的题目，做过这种大数的题目可以用Z3求解器来解决，哈哈哈哈哈哈
下面是关于Z3求解器文章的讲解
引用:https://www.cnblogs.com/hetianlab/p/13685260.html
总体来说分为一下几个步骤:
先设置变量-->然后设置限制条件 -->然后判断是否有解 -->求解并输出
设置变量:
Int - 整数
x = Int('x')
Solver对象:
我们需要先实例化一个对象，方便我们添加更多的约束对象
solver = Solver()
然后添加约束条件：
譬如：solver.add(a + 999999999 = 8888888888888)等等条件，一行添加一个约束条件，这里的约束条件就是方程等式.
具体想了解Z3的师傅直接看上面引用的文章即可.
而且这里的函数还有坑，一定要注意，一定要注意！！！
第一个坑就是，a[6]没有，第二个坑就是a[16],a[17]出现了顺序颠倒，hhhh
下面附上脚本
手写的我麻了，有没有大佬能搞个一键dump图片数据的脚本，一个一个写真的好麻烦唉-_-~~~
然后写个for循环去转换字符即可
但是你以为这就是结束了？放屁，还有a[6]字符没有搞出来，后面听别的师傅说，flag写个限制0-9,小写字母，和大写字母的爆破脚本就行，爆破第6位
然后a[6]爆破出来后，a[6]=1.
最终答案 flag{e165421110ba03099a1c039337}
解毕!!!
总结:z3yyds!!!!
标签：约束条件,BUUCTF,大数,--,然后,RE,flag,Z3 From： https://www.cnblogs.com/qsons/p/16904914.html