CTF逆向-[GWCTF 2019]babyvm-WP-虚机模拟流程反向编码和z3约束求解器解方程工具的使用

来源：https://buuoj.cn/

内容：

附件：https://pan.baidu.com/s/1FKkXN6JDI0QkGw-UE2crNA?pwd=grb0 提取码：grb0

答案：Y0u_hav3_r3v3rs3_1t!

总体思路

发现是虚机模拟

形成每个指令的逆向

找到加密值位置（有可能不止一个位置，该题就给了一个误导的）

找到命令执行的流程（也是不止一个）

逆向编写反向加密得到flag

详细步骤

查看文件信息，题目解压以后发现是各个节区，则题目本身zip文件就是样本
拖入ida64中开始动调，远程动调方法可以参考CTF逆向-[watevrCTF 2019]Timeout-WP-远程调试和修改程序当前运行位置RIP
发现有虚机模拟，则按F7逐步骤跟进
f_vm_init是虚机的初始化方法，并且以相应的操作码作为函数命名，右键创建一个struct方便后续查看
g_actions是一个全局变量，存储着需要执行的指令和值
进入f_vm1，将a1参数右键convert to struct选择我们创建的结构体

发现此处是一个操作分发，E1 E2 E3 E5是分别往虚机中赋值，E4 E7是从虚机中取值

unsigned __int64 __fastcall f_vm1(s_VMCall *a1)
{int *v_param; // [rsp+28h] [rbp-18h]unsigned __int64 v3; // [rsp+38h] [rbp-8h]v3 = __readfsqword(0x28u);v_param = (int *)(a1->actions + 2LL);switch ( *(_BYTE *)(a1->actions + 1LL) ){case 0xE1:a1->var1 = *((char *)g_input + *v_param);break;case 0xE2:a1->var2 = *((char *)g_input + *v_param);break;case 0xE3:a1->var3 = *((char *)g_input + *v_param);break;case 0xE4:*((_BYTE *)g_input + *v_param) = a1->var1;break;case 0xE5:a1->var4 = *((char *)g_input + *v_param);break;case 0xE7:*((_BYTE *)g_input + *v_param) = a1->var2;break;default:break;}a1->actions += 6LL;return __readfsqword(0x28u) ^ v3;
}

进入f_vm2发现是将var1 xor var2 存入 var1

unsigned __int64 __fastcall f_vm2_xor1and2(s_VMCall *a1)
{unsigned __int64 v2; // [rsp+18h] [rbp-8h]v2 = __readfsqword(0x28u);a1->var1 ^= a1->var2;++a1->actions;return __readfsqword(0x28u) ^ v2;
}

进入f_vm4发现是什么都不干

unsigned __int64 __fastcall f_vm4_inplace_add(s_VMCall *a1)
{unsigned __int64 v2; // [rsp+18h] [rbp-8h]v2 = __readfsqword(0x28u);++a1->actions;return __readfsqword(0x28u) ^ v2;
}

进入f_vm5发现是检查input的长度

unsigned __int64 __fastcall f_vm5_check_length(s_VMCall *a1)
{const char *v_input; // [rsp+10h] [rbp-10h]unsigned __int64 v3; // [rsp+18h] [rbp-8h]v3 = __readfsqword(0x28u);v_input = (const char *)g_input;read(0, g_input, 0x20uLL);v_input_len = strlen(v_input);if ( v_input_len != 21 ){puts("WRONG!");exit(0);}++a1->actions;return __readfsqword(0x28u) ^ v3;
}

进入f_vm6发现是var1变为 var3 + 2 * var2 + 3 * var1

unsigned __int64 __fastcall f_vm6_v3_add_2v2_add_3v1(s_VMCall *a1)
{unsigned __int64 v2; // [rsp+18h] [rbp-8h]v2 = __readfsqword(0x28u);a1->var1 = a1->var3 + 2 * a1->var2 + 3 * a1->var1;++a1->actions;return __readfsqword(0x28u) ^ v2;
}

进入f_vm7发现是将var1自乘var4

unsigned __int64 __fastcall f_vm7_inplace_multi_v4(s_VMCall *a1)
{unsigned __int64 v2; // [rsp+18h] [rbp-8h]v2 = __readfsqword(0x28u);a1->var1 *= a1->var4;++a1->actions;return __readfsqword(0x28u) ^ v2;
}

进入f_vm8发现是交换var1和var2

unsigned __int64 __fastcall f_vm8_swap_v1_v2(s_VMCall *a1)
{int var1; // [rsp+14h] [rbp-Ch]unsigned __int64 v3; // [rsp+18h] [rbp-8h]v3 = __readfsqword(0x28u);var1 = a1->var1;a1->var1 = a1->var2;a1->var2 = var1;++a1->actions;return __readfsqword(0x28u) ^ v3;
}

继续看主程序，发现f_run中是检查操作码是否是F4，是的话则停止

unsigned __int64 __fastcall f_run(s_VMCall *a1)
{unsigned __int64 v2; // [rsp+18h] [rbp-8h]v2 = __readfsqword(0x28u);a1->actions = g_actions;while ( *(_BYTE *)a1->actions != 0xF4 )f_do_next((__int64)a1);return __readfsqword(0x28u) ^ v2;
}

在f_do_next中是通过f_vm1_dispatch分发每个指令的执行

unsigned __int64 __fastcall f_do_next(s_VMCall *a1)
{int i; // [rsp+14h] [rbp-Ch]unsigned __int64 v3; // [rsp+18h] [rbp-8h]v3 = __readfsqword(0x28u);for ( i = 0; *(_BYTE *)a1->actions != *(&a1->opCode1 + 16 * i); ++i );(*((void (__fastcall **)(s_VMCall *))&a1->opFun1_dispatch + 2 * i))(a1);return __readfsqword(0x28u) ^ v3;
}

点开每个操作码对应的方法形成虚机操作列表

import z3
import structop_codes = 'F5F1E100000000F2F1E420000000F1E101000000F2F1E421000000F1E102000000F2F1E422000000F1E103000000F2F1E423000000F1E104000000F2F1E424000000F1E105000000F2F1E425000000F1E106000000F2F1E426000000F1E107000000F2F1E427000000F1E108000000F2F1E428000000F1E109000000F2F1E429000000F1E10A000000F2F1E42A000000F1E10B000000F2F1E42B000000F1E10C000000F2F1E42C000000F1E10D000000F2F1E42D000000F1E10E000000F2F1E42E000000F1E10F000000F2F1E42F000000F1E110000000F2F1E430000000F1E111000000F2F1E431000000F1E112000000F2F1E432000000F1E113000000F2F1E433000000F40000000000000000000000000000000000000000000000000000F5F1E100000000F1E201000000F2F1E400000000F1E101000000F1E202000000F2F1E401000000F1E102000000F1E203000000F2F1E402000000F1E103000000F1E204000000F2F1E403000000F1E104000000F1E205000000F2F1E404000000F1E105000000F1E206000000F2F1E405000000F1E106000000F1E207000000F1E308000000F1E50C000000F6F7F1E406000000F1E107000000F1E208000000F1E309000000F1E50C000000F6F7F1E407000000F1E108000000F1E209000000F1E30A000000F1E50C000000F6F7F1E408000000F1E10D000000F1E213000000F8F1E40D000000F1E713000000F1E10E000000F1E212000000F8F1E40E000000F1E712000000F1E10F000000F1E211000000F8F1E40F000000F1E711000000F4'
index = 0actions = []def do_func(raw):a = int(raw)if a == 0:if actions[len(actions)-1] == '':returnactions.append('')elif a == 2:actions.append(f'v1 ^= v2')elif a == 4:passelif a == 5:actions.append(f'g_input = input() # 输20位')elif a == 6:actions.append(f'v1 = v3 + 2 * v2 + 3 * v1')elif a == 7:actions.append(f'v1 *= v4')elif a == 8:actions.append(f'\nv1 ^= v2\nv2 ^= v1\nv1 ^= v2\n\n')def do_dispatch(raw):v = struct.unpack('<I', bytes.fromhex(raw[2:]))[0]action = int(raw[1])if action == 1:actions.append(f'v1 = input[{v}]')elif action == 2:actions.append(f'v2 = input[{v}]')elif action == 3:actions.append(f'v3 = input[{v}]')elif action == 4:actions.append(f'input[{v}] = v1')elif action == 5:actions.append(f'v4 = input[{v}]')elif action == 7:actions.append(f'input[{v}] = v2')else:actions.append(f'unknown {action}:{v}')def do_next():global indext = op_codes[index:]if t[0:2] == 'F1':do_dispatch(t[2:12])index += 12else:do_func(t[1])index += 2while index < len(op_codes):do_next()with open('./flow.txt', 'w', encoding='utf-8') as f:for x in actions:f.write(f'{x}\n')

发现前一段操作码输出的flag是假flag，应该以后一段的为准

g_input = input() # 输20位
v1 = input[0]
v1 ^= v2
input[32] = v1
v1 = input[1]
v1 ^= v2
input[33] = v1
v1 = input[2]
v1 ^= v2
input[34] = v1
v1 = input[3]
v1 ^= v2
input[35] = v1
v1 = input[4]
v1 ^= v2
input[36] = v1
v1 = input[5]
v1 ^= v2
input[37] = v1
v1 = input[6]
v1 ^= v2
input[38] = v1
v1 = input[7]
v1 ^= v2
input[39] = v1
v1 = input[8]
v1 ^= v2
input[40] = v1
v1 = input[9]
v1 ^= v2
input[41] = v1
v1 = input[10]
v1 ^= v2
input[42] = v1
v1 = input[11]
v1 ^= v2
input[43] = v1
v1 = input[12]
v1 ^= v2
input[44] = v1
v1 = input[13]
v1 ^= v2
input[45] = v1
v1 = input[14]
v1 ^= v2
input[46] = v1
v1 = input[15]
v1 ^= v2
input[47] = v1
v1 = input[16]
v1 ^= v2
input[48] = v1
v1 = input[17]
v1 ^= v2
input[49] = v1
v1 = input[18]
v1 ^= v2
input[50] = v1
v1 = input[19]
v1 ^= v2
input[51] = v1g_input = input() # 输20位
v1 = input[0]
v2 = input[1]
v1 ^= v2
input[0] = v1
v1 = input[1]
v2 = input[2]
v1 ^= v2
input[1] = v1
v1 = input[2]
v2 = input[3]
v1 ^= v2
input[2] = v1
v1 = input[3]
v2 = input[4]
v1 ^= v2
input[3] = v1
v1 = input[4]
v2 = input[5]
v1 ^= v2
input[4] = v1
v1 = input[5]
v2 = input[6]
v1 ^= v2
input[5] = v1
v1 = input[6]
v2 = input[7]
v3 = input[8]
v4 = input[12]
v1 = v3 + 2 * v2 + 3 * v1
v1 *= v4
input[6] = v1
v1 = input[7]
v2 = input[8]
v3 = input[9]
v4 = input[12]
v1 = v3 + 2 * v2 + 3 * v1
v1 *= v4
input[7] = v1
v1 = input[8]
v2 = input[9]
v3 = input[10]
v4 = input[12]
v1 = v3 + 2 * v2 + 3 * v1
v1 *= v4
input[8] = v1
v1 = input[13]
v2 = input[19]v1 ^= v2
v2 ^= v1
v1 ^= v2input[13] = v1
input[19] = v2
v1 = input[14]
v2 = input[18]v1 ^= v2
v2 ^= v1
v1 ^= v2input[14] = v1
input[18] = v2
v1 = input[15]
v2 = input[17]v1 ^= v2
v2 ^= v1
v1 ^= v2input[15] = v1
input[17] = v2

最终处理后发现其处理方式，得到exp

# flow.txt的第一段
v2 = 0x12
g_fake_key = 'Fz{aM{aM|}fMt~suM !!'
flag = []
for index, i in enumerate(g_fake_key):flag.append(ord(i) ^ v2)
print(''.join([chr(x) for x in flag]))
# 假的flag：This_is_not_flag_233# flow.txt的第二段
def direct_run():flag = [0 for x in range(20)]flag[0] ^= flag[1]flag[1] ^= flag[2]flag[2] ^= flag[3]flag[3] ^= flag[4]flag[4] ^= flag[5]flag[5] ^= flag[6]# v1 = input[6]# v2 = input[7]# v3 = input[8]# v4 = input[12]# v1 = v3 + 2 * v2 + 3 * v1# v1 *= v4# input[6] = v1flag[6] = flag[8] + 2 * flag[7] + 3 * flag[6]flag[6] *= flag[12]# v1 = input[7]# v2 = input[8]# v3 = input[9]# v4 = input[12]# v1 = v3 + 2 * v2 + 3 * v1# v1 *= v4# input[7] = v1flag[7] = flag[9] + 2 * flag[8] + 3 * flag[7]flag[7] *= flag[12]# v1 = input[8]# v2 = input[9]# v3 = input[10]# v4 = input[12]# v1 = v3 + 2 * v2 + 3 * v1# v1 *= v4# input[8] = v1flag[8] = flag[10] + 2 * flag[9] + 3 * flag[8]flag[8] *= flag[12]# 13和19交换# 14和18交换# 15和17交换def add_and_multi(a, b, c, d):return (c+2*b+3*a)*ddef swap(flag, index1, index2):flag[index1] ^= flag[index2]flag[index2] ^= flag[index1]flag[index1] ^= flag[index2]def reverse_flag(key):f = [x for x in key]# 注意乘法的话这里需要使用BitVec，否则无法计算约束r = [z3.BitVec(f'a{index}', 8) for index, x in enumerate(key)]swap(f, 15, 17)swap(f, 14, 18)swap(f, 13, 19)v4 = f[12]s = z3.Solver()s.add(f[8] == add_and_multi(r[8], f[9], f[10], v4))s.add(f[7] == add_and_multi(r[7], r[8], f[9], v4))s.add(f[6] == add_and_multi(r[6], r[7], r[8], v4))if s.check() != z3.sat:print('fail')returnm = s.model()for k in m:v = m[k].as_long()k = int(str(k)[1:])f[k] = vf[5] ^= f[6]f[4] ^= f[5]f[3] ^= f[4]f[2] ^= f[3]f[1] ^= f[2]f[0] ^= f[1]print(''.join([chr(x) for x in f]))g_key = '69452A370917C50B5C723376332174315F337372000000000000000000000000'
g_key = bytearray.fromhex(g_key)[0:20]
reverse_flag([ord(x) for x in g_fake_key]) # fail
reverse_flag(g_key) # Y0u_hav3_r3v3rs3_1t!

参考文档

Python反汇编方法 Python的pyc字节码反编译反汇编相关知识
CTF逆向-常用的逆向工具提取码：pnbt
B站教程中国某省队CTF集训(逆向工程部分)
- 中国某省队CTF集训(逆向工程部分)(已授权)(一)
- 基础加密方式例如 XXTEA、Base64换表
- Python库 Z3 方程式、不定式等的 约束求解
- 基础的假跳转花指令(脏字节)
- 非自然程序流程
  - 扁平化程序控制流
  - OLLVM程序流程（虚拟机壳）很难一般不考
  - ida里面按X键跟踪，寻找所有Ty为w的引用（即类型是写入的），通常就是关键位置
- 中国某省队CTF集训(逆向工程部分)(已授权)(二)
- ollydb动调去壳，upx为例子
- python的逆向和自定义虚拟指令
  - 使用pycdc 提取码：dorr 解密python编译的exe或者pyc
  - 逐条去解析用py字典手动实现的指令调用
  - C++编译的程序的逆向
- 中国某省队CTF集训(逆向工程部分)(已授权)(三)
  - 简单模运算加密
  - base58 寻找一下特别大的数，这种数通常是算法的标识，或者ida7.7版本以上自带的find crypt插件ctrl+alt+f
  - 常见的关键位置是有新的内存分配的地方通常是关键地方，或者函数中间突然return的地方也是
  - 迷宫题注意绘制出来就好
  - 动调题
    - 注意观察会执行的反调试分支，例如出现int 3，需要跳过去
基本知识
- 大小端序

更多CTF逆向题通用性做法和常用工具下载参考该博文内容：CTF逆向Reverse题的玩法