第一步 查壳
通过010Editor查看文件的标志位可以知道这是一个.EIF的可执行文件
文件标志位
具有UPX壳
第二步、脱壳
有多种方法可以脱壳，这里我们用Free UPX这个工具
其他方法可以参照我的另一篇文章：程序脱壳篇 | 乙太 (gitee.io)
第三步、IDA
脱壳后IDA64载入，直接是无法F5的，所以可以shift+F12查找字符串
双击进入，交叉引用跟踪
查看函数sub_4009AE
后面还一堆运算直接干懵逼，看了大佬的文章才发现，这是一个可以用到python中的z3库的一个约束问题，大佬z3教程特写详细，膜拜(29条消息) Z3约束器详细学习（0）—Z3安装|语句详解_z3约束求解器_Forgo7ten的博客-CSDN博客
果然做题还得靠经验才敏感
学会z3之后，这题就简单了，直接编写脚本（手动狗头，借鉴大佬）：
from z3 import *
s = Solver()
a1 = [0]*32
for i in range(32):
a1[i] = Int('a1['+str(i)+']')
s.add( 1629056 * a1[0] == 166163712 )
s.add( 6771600 * a1[1] == 731332800 )
s.add( 3682944 * a1[2] == 357245568 )
s.add( 10431000 * a1[3] == 1074393000 )
s.add( 3977328 * a1[4] == 489211344 )
s.add( 5138336 * a1[5] == 518971936 )
s.add( 7532250 * a1[7] == 406741500 )
s.add( 5551632 * a1[8] == 294236496 )
s.add( 3409728 * a1[9] == 177305856 )
s.add( 13013670 * a1[10] == 650683500 )
s.add( 6088797 * a1[11] == 298351053 )
s.add( 7884663 * a1[12] == 386348487 )
s.add( 8944053 * a1[13] == 438258597 )
s.add( 5198490 * a1[14] == 249527520 )
s.add( 4544518 * a1[15] == 445362764 )
s.add( 3645600 * a1[17] == 174988800 )
s.add( 10115280 * a1[16] == 981182160 )
s.add( 9667504 * a1[18] == 493042704 )
s.add( 5364450 * a1[19] == 257493600 )
s.add( 13464540 * a1[20] == 767478780 )
s.add( 5488432 * a1[21] == 312840624 )
s.add( 14479500 * a1[22] == 1404511500 )
s.add( 6451830 * a1[23] == 316139670 )
s.add( 6252576 * a1[24] == 619005024 )
s.add( 7763364 * a1[25] == 372641472 )
s.add( 7327320 * a1[26] == 373693320 )
s.add( 8741520 * a1[27] == 498266640 )
s.add( 8871876 * a1[28] == 452465676 )
s.add( 4086720 * a1[29] == 208422720 )
s.add( 9374400 * a1[30] == 515592000 )
s.add(5759124 * a1[31] == 719890500)
s.check()
print(s.model())
然后说一些遇到的python问题，由于我用的是python3.10所以直接pip install z3可能过时了，所以执行会出现以下问题
我重新安装pip install z3-solver才解决问题
获得输出结果之后，复制还要再写一个脚本：
a1 = [0]*32
a1[23] = 49
a1[26] = 51
a1[24] = 99
a1[11] = 49
a1[0] = 102
a1[30] = 55
a1[21] = 57
a1[1] = 108
a1[16] = 97
a1[18] = 51
a1[3] = 103
a1[13] = 49
a1[20] = 57
a1[7] = 54
a1[31] = 125
a1[29] = 51
a1[10] = 50
a1[4] = 123
a1[2] = 97
a1[8] = 53
a1[12] = 49
a1[25] = 48
a1[14] = 48
a1[28] = 51
a1[22] = 97
a1[17] = 48
a1[15] = 98
a1[19] = 48
a1[9] = 52
a1[5] = 101
a1[27] = 57
for j in range(32):
if j == 6:
continue
print(chr(a1[j]), end="")
到最后我们才发现，出题人好像还少给了一位a1[6]，大佬是用burpsuite爆破出来的a1[6]=1
所以最终flag为flag{e165421110ba03099a1c039337}
最后回来说一下一个有意思的事情，其实闲着无聊我想着去MD5md5在线解密破解,md5解密加密 (cmd5.com)解密一下这段flag是啥，结果发现原来它就是233哈哈哈！
总结
最后，声明下我借鉴得大佬的文章：(29条消息) re学习笔记（37）BUUCTF-re-[GUET-CTF2019]re Z3约束求解器_Forgo7ten的博客-CSDN博客
再写是因为自己再复现了一遍，希望加深印象，增强理解
如有错误，欢迎感谢支出，并参与讨论。
借鉴引用注明出处，谢谢理解！
