BUUCTF-[GUET-CTF2019]re(Reverse逆向)

博主： unique-Elven
发布时间：2023 年 05 月 23 日
279 次浏览
暂无评论
3589字数
分类： CTF刷题经验

# 第一步 查壳

通过010Editor查看文件的标志位可以知道这是一个.EIF的可执行文件

[ELF文件格式 - 知乎 (zhihu.com)](https://zhuanlan.zhihu.com/p/286088470)

文件标志位

![image.png](https://www.oisec.cn/usr/uploads/2023/05/4008419404.png)

具有UPX壳

![image.png](https://www.oisec.cn/usr/uploads/2023/05/1248608477.png)

# 第二步、脱壳

有多种方法可以脱壳，这里我们用Free UPX这个工具

其他方法可以参照我的另一篇文章：[程序脱壳篇 | 乙太 (gitee.io)](https://unique-yyds.gitee.io/2023/04/22/ketu/)

![image.png](https://www.oisec.cn/usr/uploads/2023/05/3280595675.png)

# 第三步、IDA

脱壳后IDA64载入，直接是无法F5的，所以可以shift+F12查找字符串

![image.png](https://www.oisec.cn/usr/uploads/2023/05/1328352527.png)

双击进入，交叉引用跟踪

![image.png](https://www.oisec.cn/usr/uploads/2023/05/2268404462.png)

查看函数**sub_4009AE**

![image.png](https://www.oisec.cn/usr/uploads/2023/05/3758877580.png)

后面还一堆运算直接干懵逼，看了大佬的文章才发现，这是一个可以用到python中的z3库的一个约束问题，大佬z3教程特写详细，膜拜[(29条消息) Z3约束器详细学习（0）—Z3安装|语句详解_z3约束求解器_Forgo7ten的博客-CSDN博客](https://blog.csdn.net/Palmer9/article/details/103738337)

果然做题还得靠经验才敏感

学会z3之后，这题就简单了，直接编写脚本（手动狗头，借鉴大佬）：

```py
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`可能过时了，所以执行会出现以下问题

![image.png](https://www.oisec.cn/usr/uploads/2023/05/6161308.png)

我重新安装`pip install z3-solver`才解决问题

获得输出结果之后，复制还要再写一个脚本：

```python
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}`

最后回来说一下一个有意思的事情，其实闲着无聊我想着去MD5[md5在线解密破解,md5解密加密 (cmd5.com)](https://www.cmd5.com/)解密一下这段flag是啥，结果发现原来它就是`233`哈哈哈！

# 总结

最后，声明下我借鉴得大佬的文章：[(29条消息) re学习笔记（37）BUUCTF-re-[GUET-CTF2019]re Z3约束求解器_Forgo7ten的博客-CSDN博客](https://blog.csdn.net/Palmer9/article/details/104210881)

再写是因为自己再复现了一遍，希望加深印象，增强理解

如有错误，欢迎感谢支出，并参与讨论。

借鉴引用注明出处，谢谢理解！

最后修改：2023 年 05 月 24 日

如果觉得我的文章对你有用，请随意赞赏

发表评论取消回复
使用cookie技术保留您的个人信息以便您下次快速评论，继续评论表示您已同意该条款

评论 *

名称 *

🎲

邮箱 *

地址

affgrzbhop
文章的叙述风格独特，用词精准，让人回味无穷。
adtmqpnohc
文章紧扣主题，观点鲜明，展现出深刻的思考维度。
zvbxxphjlf
选材新颖独特，通过细节描写赋予主题鲜活生命力。
owculzhvhb
文章结构紧凑，层次分明，逻辑严密，让人一读即懂。
zelkzjiisy
终极关怀的缺失可尝试补充升华。

BUUCTF-[GUET-CTF2019]re(Reverse逆向)

unique-Elven • 2023 年 05 月 23 日

# 第一步 查壳

通过010Editor查看文件的标志位可以知道这是一个.EIF的可执行文件

[ELF文件格式 - 知乎 (zhihu.com)](https://zhuanlan.zhihu.com/p/286088470)

文件标志位

![image.png](https://www.oisec.cn/usr/uploads/2023/05/4008419404.png)

具有UPX壳

![image.png](https://www.oisec.cn/usr/uploads/2023/05/1248608477.png)

# 第二步、脱壳

有多种方法可以脱壳，这里我们用Free UPX这个工具

其他方法可以参照我的另一篇文章：[程序脱壳篇 | 乙太 (gitee.io)](https://unique-yyds.gitee.io/2023/04/22/ketu/)

![image.png](https://www.oisec.cn/usr/uploads/2023/05/3280595675.png)

# 第三步、IDA

脱壳后IDA64载入，直接是无法F5的，所以可以shift+F12查找字符串

![image.png](https://www.oisec.cn/usr/uploads/2023/05/1328352527.png)

双击进入，交叉引用跟踪

![image.png](https://www.oisec.cn/usr/uploads/2023/05/2268404462.png)

查看函数**sub_4009AE**

![image.png](https://www.oisec.cn/usr/uploads/2023/05/3758877580.png)

果然做题还得靠经验才敏感

学会z3之后，这题就简单了，直接编写脚本（手动狗头，借鉴大佬）：

```py
from z3 import *
s = Solver()
a1 = [0]*32
for i in range(32):
    a1[i] = Int('a1['+str(i)+']')

然后说一些遇到的python问题，由于我用的是python3.10所以直接`pip install z3`可能过时了，所以执行会出现以下问题

![image.png](https://www.oisec.cn/usr/uploads/2023/05/6161308.png)

我重新安装`pip install z3-solver`才解决问题

获得输出结果之后，复制还要再写一个脚本：

到最后我们才发现，出题人好像还少给了一位a1[6]，大佬是用burpsuite爆破出来的a1[6]=1

所以最终flag为`flag{e165421110ba03099a1c039337}`

# 总结

再写是因为自己再复现了一遍，希望加深印象，增强理解

如有错误，欢迎感谢支出，并参与讨论。

借鉴引用注明出处，谢谢理解！

BUUCTF-[GUET-CTF2019]re(Reverse逆向)

发表评论取消回复
使用cookie技术保留您的个人信息以便您下次快速评论，继续评论表示您已同意该条款

BUUCTF-CrackRTF(Reverse逆向)

BUUCTF-[2019红帽杯]easyRE(Reverse逆向)

SSRF

服装生产销售管理系统

恶意代码分析入门--静态分析（chapter1_Lab01-01）

014-Splish 的 write up

2023有关金砖的练习题（云启平台）

如何快速定位关键点并爆破——不修改代码实现破解2

逆向学习第一步--C语言笔记

软件保护技术-程序脱壳篇-逆向工程学习记录

BUUCTF-[GUET-CTF2019]re(Reverse逆向)

发表评论 取消回复 使用cookie技术保留您的个人信息以便您下次快速评论，继续评论表示您已同意该条款

BUUCTF-[GUET-CTF2019]re(Reverse逆向)

发表评论取消回复
使用cookie技术保留您的个人信息以便您下次快速评论，继续评论表示您已同意该条款