CTF逆向：基础VM的三大解法剖析

一、VM核心原理速览

VM题型简介

VM（Virtual Machine）类题目在CTF逆向中常见，其特点如下：

• 程序通常有自己一套循环的执行程序流
• 核心结构包含虚拟指令分发器(opcode)和加密逻辑
• opcode由操作数和操作组成的大串数据（通常由成百上千个byte组成）

破局思路

1. 关键定位：找到虚拟指令分发器(opcode)
2. 加密逻辑：分析循环加密过程
3. 模拟重建：模拟执行流进行爆破或解密

二、三种解法概述

解法一：传统手撕

• 保存整个执行流程
• 逆向操作，从加密结果倒推flag

解法二：正向Z3约束求解

• 模拟加密过程
• 使用Z3约束求解得到flag

解法三：插桩爆破

• 利用gbd或frida插桩
• 针对单字节或双字节进行爆破

三、解题实战（以isctf2022为例）

1. 提取opcode

1. 在IDA中定位到opcode变量（示例中为v8）
2. 提取方法：
   • 手动提取：选择变量，使用shift+8提取（24个变量，每个16 byte）
   • IDAPython脚本提取（示例未展示具体脚本）

2. 复现执行流

• 注意坑点：某些操作的实际实现可能与表面不同（如[i-1]而非[1]）
• 需要仔细对照汇编代码

3. 具体解法实现

解法一：逆向手撕

# 示例exp思路
opcode = [...]  # 存储提取的opcode
enc = [...]     # 加密结果

# 从后往前解密
for i in range(len(opcode)-1, -1, -1):
    # 逆向操作：+变-，-变+，^保持不变
    # 注意异或优先级问题
    pass

解法二：Z3约束求解

关键点：

• 必须创建flag副本进行encode操作
• 避免符号变量导致的优先级混乱

from z3 import *

def encode(flag, opcode):
    # 实现正向加密过程
    pass

solver = Solver()
flag = [BitVec(f'flag_{i}', 8) for i in range(len(enc))]
encoded_flag = encode(flag.copy(), opcode)  # 必须使用副本

for i in range(len(enc)):
    solver.add(encoded_flag[i] == enc[i])

if solver.check() == sat:
    model = solver.model()
    # 提取flag

解法三：frida插桩爆破

// frida脚本示例
Interceptor.attach(target_function, {
    onEnter: function(args) {
        // 修改参数进行爆破
    },
    onLeave: function(retval) {
        // 检查结果
    }
});

四、高难度VM应对策略

对于2024年强网杯等高难度VM题目：

1. 当找不到opcode和中间执行流时
2. 当前思路主要是无脑爆破
3. 需要提升静态分析能力（大佬可以手撕）

五、总结

1. 基础VM：三种解法各有优劣，Z3约束求解最通用
2. 关键点：
   • 准确提取opcode
   • 正确复现执行流
   • 注意操作优先级和边界条件
3. 进阶：需要积累更多VM分析经验，提升静态分析能力

六、参考资料

1. 示例题目：isctf2022基础VM题
2. 推荐博客：swdd的VM分析文章（原文中提到但未具体说明）
3. 强网杯2024 VM题目（高难度示例）