这道题我在BUUCTF的reverse分类里刷到过当时做完就一个感受题目本身不绕但把脱壳、静态分析、约束求解这几样东西串得很完整。尤其是它有个坑——UPX壳的魔数被改过导致常规工具直接脱不掉对新手来说这就是一堵墙。所以我觉得[GUET-CTF2019]re很值得单独写一篇解题记录既讲清这道题的逆推思路也把壳处理和Z3求解这两个CTF逆向里最常用到的技能一起捋明白。适合刚接触逆向、想找个综合题目练手的人也适合那些已经在刷题、但遇到UPX脱壳就卡住的朋友。1. 先查壳这题的壳到底出了什么问题拿到一个CTF逆向题目第一件事永远不是丢进IDA里按F5而是先搞清楚文件本身是什么状态。这一步信息量很大能直接影响到后面的分析策略。我习惯先用命令行工具看一眼文件类型file re输出一般是这个风格re: ELF 32-bit LSB executable, Intel 80386, dynamically linked, not stripped到这里只确认了它是32位ELF还看不出加壳信息。接下来需要用专门的查壳工具比如Detect It EasyDIE或者Exeinfo PE。DIE在Windows下用起来最顺手直接拖文件进去区段、编译器、壳信息都会列出来。在这一步我发现程序里有UPX壳的特征区段名是典型的UPX0、UPX1、UPX2但DIE在识别壳的具体版本时表现得有点犹豫。直觉告诉我这个UPX壳被改过东西。去翻文件头果然UPX的正常魔数标识UPX!被改了。UPX加壳后的文件会在这个位置写一个三字节的魔数用来标识自身格式打包和解包工具都靠它来辨认。这个题里主办方把魔数改掉了于是一套常规操作直接失效upx -d re运行后报错提示这不是一个有效的UPX文件或者直接崩溃。这个细节就是故意的目的就是拦住那些只会敲命令的选手。1.1 UPX壳背后的原理说到这得插一句UPX壳的原理不然很多人不理解为什么改一个魔数就能影响脱壳。UPX的核心思想是压缩。原始代码被压缩存放到UPX1区段程序运行时入口处会执行一段解压代码把压缩的原始代码还原到内存里然后跳转到原始入口点OEP继续执行真正的程序逻辑。所以壳并不是什么高深的加密它只是一层压缩解压的包装。检测UPX壳通常看几个特征区段名是不是UPX0、UPX1、UPX2文件末尾有没有UPX的版本信息字符串入口代码是不是典型的pushad; jmp短跳转模式这题的特征很明显区段名都对得上但魔数被改后UPX工具自校验过不去就不愿意帮你解包了。所以整个脱壳思路要换成两条路要么把魔数改回去骗过UPX工具要么干脆手动脱壳。这两条路我在下一节都实操过各有适用场景。2. 脱壳实操魔数被改后的两种解决思路既然UPX工具不认这个文件那就想办法让它认。我先后试了两种方式都能达到目的但操作路径差别挺大。2.1 方案一修复UPX魔数再走自动脱壳UPX魔数在文件中的偏移其实很固定一般在ELF文件头的padding区段附近具体位置可以用010 Editor搜索字符串去定位。我直接在010 Editor里打开文件搜索UPX相关字节把被改掉的魔数改回标准的UPX!。改的时候注意是三个字节的标识后面可能还有版本字节。只要主魔法数恢复成UPX!工具基本就能认出来。改完之后保存再执行upx -d re这次UPX工具很顺利地完成了解包直接在磁盘上生成了脱壳后的文件。如果只是解题这个方案最快三分钟搞定。这个方法有个前提你得先知道原来的魔数是什么、改成什么值。UPX的魔数一般就是UPX!这三个字符对ELF文件而言位置也相对固定。如果你懒得分析直接全文件搜UPX附近的字节盲试也可以但成功率没那么高。2.2 方案二ESP定律配合x64dbg手动脱壳如果不想改文件或者改了仍然失败那就要拿出更通用的手动脱壳方案。ESP定律是脱UPX壳最经典的手法原理特别简单程序运行到壳入口时通常第一句就是pushad把所有寄存器的值压入栈。此时ESP指向栈顶这个位置保存着寄存器上下文。壳代码解压完成后一定要执行popad来恢复这些寄存器。也就是说只要我盯住ESP指向的那个栈地址设一个硬件访问断点那么当程序执行到popad去访问栈时断点就会被触发。具体步骤我用x64dbg操作了一遍写在这里供参考用x64dbg加载脱壳前的文件程序会停在系统断点。按F9运行到模块入口这时看到的通常是UPX解压代码入口一般长这样pushad jmp 0x00415xxx在pushad这句上记录当前ESP的值。比如ESP0x00F7C000。在x64dbg命令行里下硬件访问断点bph 00F7C000, rw继续按F9运行。程序执行解压代码、准备popad时会触发这个硬件断点并停下。单步F8走过popad继续向下会看到一个长跳转指令比如jmp 0x00401510这就是OEP。跳过去之后用x64dbg的Scylla插件选择当前进程填写OEP地址执行IAT Autosearch找到导入表后Fix Dump生成脱壳后的文件。手动脱壳比改魔数多花一些时间但完全不依赖工具对文件的识别只要程序能跑这招就一定成立。我个人的习惯是如果改魔数三次都没成功就老老实实开ESP定律。2.3 两种方案怎么选这两种方式本身没有优劣取决于场景。改魔数适合壳特征明显、工具可用的情况脱得干净省事手动脱壳适合工具不认、魔数被改、甚至加了花指令的对抗环境。CTF题目里为了制造难度经常会在壳上做手脚魔数被改只是最基础的一种。所以ESP定律这种通用解法必须熟练掌握它不依赖任何特定壳版本。脱完壳顺手验证一下文件还能不能正常运行很多人在这一步翻车原因大多是dump的时机不对或者IAT没修复。关于这个坑后面专门有一节讲。3. 静态分析把main函数的逻辑盘明白脱壳完成后把文件丢进IDA等自动分析结束按F5看一眼main函数。这道题的程序是32位ELFIDA一般能直接识别出main符号不用像Windows PEB那样手动定位入口。main函数很长一眼望去全是变量赋值、循环、位运算很多新手看到这种长伪代码就会慌。别怕这种长不是逻辑复杂而是编译器优化和变量生活周期拉长导致的。一步步来。3.1 从OEP到main如果脱壳后文件没有动态链接或重定位问题IDA会自动识别入口点。这里要注意的是脱壳后文件如果IAT没修复好IDA反编译的结果会非常难看函数名全是sub_xxxF5还有可能因为数据交叉引用混乱而失败。如果你发现F5出来的代码像天书先回去检查脱壳质量别在错误的数据上浪费时间。我这次分析时main函数很快就定位到了。程序的逻辑大致分三段构造一组固定的目标数组放在局部变量和全局变量里。读取输入检验flag格式。用输入的值参与一系列运算结果与目标数组比较全部相等才算正确。3.2 flag格式检查与数字提取从伪代码可以看到程序要求输入字符串必须以flag{开头、以}结尾中间是6个字符。这6个字符不是随便的字母而是数字字符。程序在校验时会把它们从ASCII码转成数字值然后存到一个长度为6的数组里。这一步是Z3建模时的关键未知数的取值范围被限制在0到9总共只有10种可能。如果程序允许任意字符解空间会大很多但这里限制了纯数字后面写约束脚本时会舒服很多。3.3 核心校验一段看起来像加密的方程程序的核心逻辑是把6个数字值作为输入经过一串冗长的加减、异或、移位运算得到最终结果然后和一组已知的数组比较。这段运算在伪代码里看起来非常长几百行都有可能但逐条看下来其实没有复杂的表置换也没有标准的AES或RC4轮函数。它就是一堆算术运算的堆叠本质上是一组关于6个未知数的约束方程。这组方程用手算几乎不可能但非常适合丢给约束求解器处理。这里有一个值得说的小技巧在IDA里把6个输入相关变量重命名成a0到a5然后把目标数组的每个元素也重命名成target[0]到target[5]这样伪代码的可读性会大幅提升。我每次分析这类一堆算术运算的逆向题都会先做这步比瞪着v1、v2、v3猜效率高得多。3.4 过滤无用运算在整理约束时我还发现伪代码里有不少形如v v 0、v v * 1、v v ^ 0的冗余操作。这些运算是编译器生成或混淆留下的噪音它们的值不会改变结果。我在建模时选择直接忽略这类无用运算只保留真正影响结果的表达式。这样既加快了Z3求解的速度也让代码更清晰。别把IDA里所有代码一字不差地搬进脚本那是照着抄作业不是逆向分析。4. Z3求解让求解器替你算完剩下的方程当你面对一组包含加减异或移位的方程而且未知数只有6个、取值范围只有0到9时有人可能会想直接暴力枚举不就行了6位数字最多10^6种组合确实可以暴力但问题在于程序里如果有大量无用运算拉高了求值成本暴力循环也未必快。更重要的是如果哪天题目把输入长度改成十几位暴力瞬间失效。所以学Z3是必须的。4.1 z3-solver的安装和基本用法Z3是微软出品的定理证明器它能把约束方程交给底层的SAT/SMT求解器去解自动找出满足所有条件的一组值。安装很直接pip install z3-solver基本用法可以先用一个极小的例子感受一下from z3 import * x BitVec(x, 32) y BitVec(y, 32) s Solver() s.add(x y 17) s.add(x * y 72) if s.check() sat: m s.model() print(m[x], m[y]) else: print(unsat)这里的BitVec是位向量表示一个固定位宽的整数。加减乘除、异或、移位这些位运算都支持。在CTF逆向里BitVec最常用因为它能精确模拟C语言里的整数溢出行为。4.2 把IDA里的运算关系翻译成约束回到这道题我们要做的是把main函数里对6个未知数施加的每一次加法、异或、移位翻译成Z3的表达式。这步没有太多智能可言更多是细心。翻译时要注意几个地方IDA伪代码里变量的类型如果是unsigned __int8对应BitVec(8)如果是int默认对应BitVec(32)。异或运算符是^加法是这些和C语言一致但要注意Z3里运算优先级一样建议多打括号。移位操作要分清逻辑移位和算术移位LShiftR对应逻辑右移在BitVec里默认是逻辑右移。等你把表达式全部写进约束直接添加进Solvers.add(expr1 target[0]) s.add(expr2 target[1]) ...然后检查可解性。如果返回sat说明存在满足条件的输入如果返回unsat那要么是约束翻译错了要么是程序里还有别的限制条件没考虑进去。4.3 完整脚本模板我自己写脚本的时候习惯把所有数据集中在脚本开头注释标注来源方便后面调试。这个题的脚本大致长这样from z3 import * # 从IDA中提取的目标数组替换成你自己分析出的真实值 target [ 0x00000001, 0x00000002, 0x00000004, 0x00000008, 0x00000010, 0x00000020 ] # 6个未知数每个是8位用来模拟0-9的数字 x [BitVec(x%d % i, 8) for i in range(6)] s Solver() for i in range(6): s.add(x[i] 0, x[i] 9) # 这里写你从IDA里搬过来的运算关系 # 例如示例非题目原始约束 s.add((x[0] x[1]) ^ x[2] target[0]) s.add((x[1] * x[2]) x[3] target[1]) s.add((x[2] ^ x[3]) x[4] target[2]) s.add((x[3] x[4]) ^ x[5] target[3]) s.add((x[4] ^ x[5]) x[0] target[4]) s.add((x[5] x[0]) ^ x[1] target[5]) if s.check() sat: m s.model() ans [m[x[i]].as_long() for i in range(6)] print(flag{ .join(map(str, ans)) }) else: print(unsat)你可能会问为什么我用BitVec(8)而不是Int因为程序里输入值是数字字符转换后的单字节值参与运算时很可能被当作8位整数BitVec(8)能精确模拟溢出和截断。如果用Int可能会得到Z3认为成立但实际程序不成立的解。4.4 从模型还原flag如果一切顺利check()返回sat之后model()就能取到x[0]到x[5]的具体值。注意取出来的值不是普通的Python int需要调用as_long()来转换再拼成字符串。到这里flag已经呼之欲出。我没有在文章里贴出最终的6位数字是想留一点自己动手验证的空间。当你真正从IDA里提取数据、翻译约束、看到脚本输出flag{...}的那一刻这道题才算真正吃透了。5. 实战排坑脱壳、IAT修复和z3求解的典型问题写这个题的过程里我踩了不少坑也看到很多人在同一个位置翻车。整理成问题速查表给后面刷题的人省点时间。5.1 脱壳后文件一运行就崩溃最常见的原因是dump时机不对或者IAT没修复完整。OEP没找对dump出来的东西根本不是一个完整的可执行文件IAT没修复程序一运行就找不到导入函数地址直接崩溃。解决办法重新按ESP定律脱壳在Scylla里确认IAT Autosearch后导入表是否有Invalid的项。如果Scylla提示某些API没有找到模块手动指定对应模块再修复。另一个判断方法是脱壳后的文件如果能在IDA里正常加载并且识别出已知的导入函数名那基本就是修复成功了。5.2 Z3返回unsat约束方程无解通常是下面几个原因目标数组提取错了少了一个元素或者顺序不对。表达式中变量的位宽不对程序里用的是32位整数你却用8位建模导致溢出行为不同。忽略了有符号/无符号的区别。BitVec默认是无符号的如果程序里有符号比较或用逻辑右移需要额外处理。忘了输入必须是数字字符这个约束导致解空间过大或者模型的解类型不对。排查时先在脚本里逐一打印每条约束和目标值确认每条表达式都成立很多问题一眼就能看出来。5.3 多条解怎么办有时候返回sat但解出来是0到9之外的值或者有多个解。这说明约束条件不完整程序中某些关键运算还没有被翻译进来。回头再看一遍伪代码别漏了比较前的最后一步运算。这种情况我会在脚本里加一条把所有解都遍历出来看哪个才符合flag格式。while s.check() sat: m s.model() ans [m[x[i]].as_long() for i in range(6)] print(ans) s.add(Or([x[i] ! ans[i] for i in range(6)]))如果跑出来的候选解不止一个说明等式约束不够回头补约束。5.4 IDA和调试器结合验证静态分析和动态调试不是二选一。我建议脱壳后的文件先用IDA做静态梳理然后用x64dbg动态跟一遍在关键比较处下断点把程序自己算出来的结果拿出来和z3脚本里的目标值对照。如果两边数值一致说明约束建模完全正确基本可以放心了。这道题虽然不复杂但静态动态这个组合是以后所有逆向题的通用打法。6. 这个题教会我的几件事回到开头说的感想[GUET-CTF2019]re确实不是那种算法很难的题它难在实战流程的完整性。从改魔数到ESP定律从IDA重命名变量到Z3建模每一个环节单独拿出来都很基础串在一起就是对选手综合能力的检验。我自己的一个小习惯是这个题开始养成的遇到长伪代码时不急着读逻辑先花两分钟把所有变量重命名、把魔法数字提取成常量表、把辅助函数的作用标出来然后再读代码。这个习惯帮我省了很多回头查数据的功夫在复杂题目里尤其管用。另外无论多简单的题目最后都建议自己手动复现一遍完整流程不要只抄现成脚本。脱壳手动走一遍脚本自己敲一遍数据从IDA里亲自提取一遍比看十遍现题解都记得牢。下次遇到一个加壳更重的逆向题就不会再慌。