CTF逆向实战：UPX魔数修复与Z3求解完整解析

这道题我在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 Easy（DIE）或者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操作了一遍，写在这里供参考：

1. 用x64dbg加载脱壳前的文件，程序会停在系统断点。
2. 按F9运行到模块入口，这时看到的通常是UPX解压代码入口，一般长这样：

pushad jmp 0x00415xxx

3. 在pushad这句上，记录当前ESP的值。比如ESP=0x00F7C000。
4. 在x64dbg命令行里下硬件访问断点：

bph 00F7C000, rw

5. 继续按F9运行。程序执行解压代码、准备popad时，会触发这个硬件断点并停下。
6. 单步F8，走过popad，继续向下，会看到一个长跳转指令，比如jmp 0x00401510，这就是OEP。
7. 跳过去之后，用x64dbg的Scylla插件，选择当前进程，填写OEP地址，执行IAT Autosearch，找到导入表后，Fix Dump生成脱壳后的文件。

手动脱壳比改魔数多花一些时间，但完全不依赖工具对文件的识别，只要程序能跑，这招就一定成立。我个人的习惯是：如果改魔数三次都没成功，就老老实实开ESP定律。

2.3 两种方案怎么选

这两种方式本身没有优劣，取决于场景。改魔数适合"壳特征明显、工具可用"的情况，脱得干净省事；手动脱壳适合"工具不认、魔数被改、甚至加了花指令"的对抗环境。CTF题目里为了制造难度，经常会在壳上做手脚，魔数被改只是最基础的一种。所以ESP定律这种通用解法必须熟练掌握，它不依赖任何特定壳版本。

脱完壳顺手验证一下文件还能不能正常运行，很多人在这一步翻车，原因大多是dump的时机不对，或者IAT没修复。关于这个坑，后面专门有一节讲。

3. 静态分析：把main函数的逻辑盘明白

脱壳完成后，把文件丢进IDA，等自动分析结束，按F5看一眼main函数。这道题的程序是32位ELF，IDA一般能直接识别出main符号，不用像Windows PEB那样手动定位入口。

main函数很长，一眼望去全是变量赋值、循环、位运算，很多新手看到这种长伪代码就会慌。别怕，这种长不是逻辑复杂，而是编译器优化和变量生活周期拉长导致的。一步步来。

3.1 从OEP到main

如果脱壳后文件没有动态链接或重定位问题，IDA会自动识别入口点。这里要注意的是，脱壳后文件如果IAT没修复好，IDA反编译的结果会非常难看，函数名全是sub_xxx，F5还有可能因为数据交叉引用混乱而失败。如果你发现F5出来的代码像天书，先回去检查脱壳质量，别在错误的数据上浪费时间。

我这次分析时，main函数很快就定位到了。程序的逻辑大致分三段：

1. 构造一组固定的目标数组（放在局部变量和全局变量里）。
2. 读取输入，检验flag格式。
3. 用输入的值参与一系列运算，结果与目标数组比较，全部相等才算正确。

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里默认是逻辑右移。

等你把表达式全部写进约束，直接添加进Solver：

s.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

约束方程无解，通常是下面几个原因：

1. 目标数组提取错了，少了一个元素或者顺序不对。
2. 表达式中变量的位宽不对，程序里用的是32位整数，你却用8位建模，导致溢出行为不同。
3. 忽略了有符号/无符号的区别。BitVec默认是无符号的，如果程序里有符号比较或用逻辑右移，需要额外处理。
4. 忘了"输入必须是数字字符"这个约束，导致解空间过大或者模型的解类型不对。

排查时先在脚本里逐一打印每条约束和目标值，确认每条表达式都成立，很多问题一眼就能看出来。

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里亲自提取一遍，比看十遍现题解都记得牢。下次遇到一个加壳更重的逆向题，就不会再慌。