re学习笔记（37）BUUCTF-re-[GUET-CTF2019]re Z3约束求解器

推荐肉丝r0ysue课程（包含安卓逆向与js逆向）：

新手一枚，如有错误（不足）请指正，谢谢！！
个人博客：点击进入
题目链接：[GUET-CTF2019]re
题目下载：点击下载

IDA64位载入

大概率被加壳，使用exeinfope查看

upx壳，使用官方upx脱壳

脱壳后IDA64载入，shift+F12查找字符串

找到关键代码

查看sub_4009AE()函数

典型z3约束器求解题
（当然你想一个个挨个手动算的话也行……）
z3安装请查看
linux笔记 CTF-pwn环境搭建
Z3约束器详细学习（0）—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())

之后提取出数据，转化为字符输出就好
因为没有a1[6]，所以跳过

a1 = [0]*32
a1[31] = 125
a1[30] = 55
a1[29] = 51
a1[28] = 51
a1[27] = 57
a1[26] = 51
a1[25] = 48
a1[24] = 99
a1[23] = 49
a1[22] = 97
a1[21] = 57
a1[20] = 57
a1[19] = 48
a1[18] = 51
a1[16] = 97
a1[17] = 48
a1[15] = 98
a1[14] = 48
a1[13] = 49
a1[12] = 49
a1[11] = 49
a1[10] = 50
a1[9] = 52
a1[8] = 53
a1[7] = 54
a1[5] = 101
a1[4] = 123
a1[3] = 103
a1[2] = 97
a1[1] = 108
a1[0] = 102
for i in range(32):if i == 6:continueprint(chr(a1[i]), end="")

出题人少给了一位a1[6]，
@羊毛羊指正使用burp爆破出来a1[6]=1
所以最终flag为flag{e165421110ba03099a1c039337}

re学习笔记（37）BUUCTF-re-[GUET-CTF2019]re Z3约束求解器相关推荐

【python环境下Z3约束求解器学习笔记】And和Or的用法
在Z3约束求解器中,我们可能需要寻找同时满足两个条件的模型,也可能需要寻找满足两个条件中一个条件的模型,这个时候,我们可以借助And方法和Or方法来实现引入我们先来举一个简单的例子当我们想要查找 ...
Building Worlds In Unreal 学习笔记——07-11 岩石树落木灌木绘制/溪水着色器/潮湿与焦散贴花/后处理
Building Worlds In Unreal 学习笔记--07-11 岩石树落木灌木绘制/溪水着色器/潮湿与焦散贴花/后处理 Lec07 岩石与树 Rocks and Trees 1 Folia ...
影像组学视频学习笔记(37)-机器学习模型判断脑卒中发病时间(文献报告)、Li‘s have a solution and plan.
作者:北欧森林链接:https://www.jianshu.com/p/3e7a2c84288e 来源:简书,已获授权转载 RadiomicsWorld.com "影像组学世界" ...
学习笔记(37):Python实战编程-yield实现生成器
立即学习:https://edu.csdn.net/course/play/19711/255579?utm_source=blogtoedu 1.yield = return + generator ...
安卓学习笔记37：利用OpenGL ES绘制平面图形
文章目录零.学习目标一.OpenGL概述二.了解三维直角坐标系三.案例演示 - 绘制三角形 (一)运行效果 (二)实现步骤 1.创建安卓应用[DrawTriangle] 2.建模:创建三角形类 ...
机器学习李宏毅学习笔记37
文章目录前言一.ChatGPT做的事情二.ChatGPT基础介绍三.ChatGPT带来的研究问题总结前言 ChatGPT简单原理介绍一.ChatGPT做的事情 Chatgpt以句子为输入 ...
iOS学习笔记37 时间和日期计算
###一.时间和日期计算我们在应用开发中,时常需要和时间打交道,比如获取当前时间,获取两个时间点相隔的时间等等,在iOS开发中与时间相关的类有如下几个: NSDate:表示一个绝对的时间点 NSTi ...
《第一行代码》学习笔记37－服务Service（4）
一个比较完整的自定义AsyncTask写成如下: class DownloadTask extends AsyncTask<Void, Integer, Boolean> {@Overri ...
大数据学习笔记37：Hive - 复杂数据类型
文章目录一.复杂数据类型二.数组类型(array)实战 (一)案例1.单列数组 1.创建文本文件array1.txt 2.将文件上传到HDFS的/a1目录 3.基于/a1目录创建hive外部表a1 ...

re学习笔记（37）BUUCTF-re-[GUET-CTF2019]re Z3约束求解器

re学习笔记（37）BUUCTF-re-[GUET-CTF2019]re Z3约束求解器相关推荐

最新文章

热门文章