vm虚拟机逆向---[GWCTF 2019]babyvm 复现【详解】-编程知识

文章目录

前言
题目分析
- CD1
- - mov指令
  - xor指令and其他指令
- E0B
- F83
汇编提取
编写exp

前言

好难。大家都觉得简单，就我觉得难是吧，，，，，

题目分析

在这里插入图片描述
、

在这里插入图片描述

代码看着挺少，三个主要函数，一开始好像是sub_CD1的，调试的时候变了，不影响。

还是一样的几个技巧，返回类型可以改成 void；形参可以改成_DWORD *reg 名称什么的也可以改改，问题也不大，方便观看而已。

CD1

在这里插入图片描述

分析下指令。

mov指令

在这里插入图片描述

这里推测是我们的输入，索引就是opcode，（reg+2）就是索引 i ；最后 i += 6；

xor指令and其他指令

在这里插入图片描述
很明显的xor了。下面应该都挺明显的，

在这里插入图片描述

计算输出flag的长度同21比较，理解为一个cmp eax ， 21这样

在这里插入图片描述

一个nop指令，单纯的 rip+1

在这里插入图片描述

mul指令，乘法 i += 2

在这里插入图片描述

做一个交换，。swap

在这里插入图片描述

一处运算。

到这里指令就分析完了。

E0B

在这里插入图片描述

一个while 一直读取opcode的数据，直到 0xF4为止，就是一个调度器的作用

F83

在这里插入图片描述

一处比较，值得注意的是，验证的数据是错误的，真正的数据需要通过交叉引用找出，
在这里插入图片描述

f = [0x69, 0x45, 0x2A, 0x37, 0x09, 0x17, 0xC5, 0x0B, 0x5C, 0x72, 0x33, 0x76, 0x33, 0x21, 0x74, 0x31, 0x5F, 0x33, 0x73, 0x72]

汇编提取

分析完程序后，写个exp先将伪汇编提出来。

opcode = [0xF5, 0xF1, 0xE1, 0x00, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4,0x20, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x01, 0x00, 0x00, 0x00,0xF2, 0xF1, 0xE4, 0x21, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x02,0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x22, 0x00, 0x00, 0x00,0xF1, 0xE1, 0x03, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x23,0x00, 0x00, 0x00, 0xF1, 0xE1, 0x04, 0x00, 0x00, 0x00, 0xF2,0xF1, 0xE4, 0x24, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x05, 0x00,0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x25, 0x00, 0x00, 0x00, 0xF1,0xE1, 0x06, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x26, 0x00,0x00, 0x00, 0xF1, 0xE1, 0x07, 0x00, 0x00, 0x00, 0xF2, 0xF1,0xE4, 0x27, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x08, 0x00, 0x00,0x00, 0xF2, 0xF1, 0xE4, 0x28, 0x00, 0x00, 0x00, 0xF1, 0xE1,0x09, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x29, 0x00, 0x00,0x00, 0xF1, 0xE1, 0x0A, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4,0x2A, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x0B, 0x00, 0x00, 0x00,0xF2, 0xF1, 0xE4, 0x2B, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x0C,0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x2C, 0x00, 0x00, 0x00,0xF1, 0xE1, 0x0D, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x2D,0x00, 0x00, 0x00, 0xF1, 0xE1, 0x0E, 0x00, 0x00, 0x00, 0xF2,0xF1, 0xE4, 0x2E, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x0F, 0x00,0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x2F, 0x00, 0x00, 0x00, 0xF1,0xE1, 0x10, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x30, 0x00,0x00, 0x00, 0xF1, 0xE1, 0x11, 0x00, 0x00, 0x00, 0xF2, 0xF1,0xE4, 0x31, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x12, 0x00, 0x00,0x00, 0xF2, 0xF1, 0xE4, 0x32, 0x00, 0x00, 0x00, 0xF1, 0xE1,0x13, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x33, 0x00, 0x00,0x00, 0xF4, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF5, 0xF1,0xE1, 0x00, 0x00, 0x00, 0x00, 0xF1, 0xE2, 0x01, 0x00, 0x00,0x00, 0xF2, 0xF1, 0xE4, 0x00, 0x00, 0x00, 0x00, 0xF1, 0xE1,0x01, 0x00, 0x00, 0x00, 0xF1, 0xE2, 0x02, 0x00, 0x00, 0x00,0xF2, 0xF1, 0xE4, 0x01, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x02,0x00, 0x00, 0x00, 0xF1, 0xE2, 0x03, 0x00, 0x00, 0x00, 0xF2,0xF1, 0xE4, 0x02, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x03, 0x00,0x00, 0x00, 0xF1, 0xE2, 0x04, 0x00, 0x00, 0x00, 0xF2, 0xF1,0xE4, 0x03, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x04, 0x00, 0x00,0x00, 0xF1, 0xE2, 0x05, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4,0x04, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x05, 0x00, 0x00, 0x00,0xF1, 0xE2, 0x06, 0x00, 0x00, 0x00, 0xF2, 0xF1, 0xE4, 0x05,0x00, 0x00, 0x00, 0xF1, 0xE1, 0x06, 0x00, 0x00, 0x00, 0xF1,0xE2, 0x07, 0x00, 0x00, 0x00, 0xF1, 0xE3, 0x08, 0x00, 0x00,0x00, 0xF1, 0xE5, 0x0C, 0x00, 0x00, 0x00, 0xF6, 0xF7, 0xF1,0xE4, 0x06, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x07, 0x00, 0x00,0x00, 0xF1, 0xE2, 0x08, 0x00, 0x00, 0x00, 0xF1, 0xE3, 0x09,0x00, 0x00, 0x00, 0xF1, 0xE5, 0x0C, 0x00, 0x00, 0x00, 0xF6,0xF7, 0xF1, 0xE4, 0x07, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x08,0x00, 0x00, 0x00, 0xF1, 0xE2, 0x09, 0x00, 0x00, 0x00, 0xF1,0xE3, 0x0A, 0x00, 0x00, 0x00, 0xF1, 0xE5, 0x0C, 0x00, 0x00,0x00, 0xF6, 0xF7, 0xF1, 0xE4, 0x08, 0x00, 0x00, 0x00, 0xF1,0xE1, 0x0D, 0x00, 0x00, 0x00, 0xF1, 0xE2, 0x13, 0x00, 0x00,0x00, 0xF8, 0xF1, 0xE4, 0x0D, 0x00, 0x00, 0x00, 0xF1, 0xE7,0x13, 0x00, 0x00, 0x00, 0xF1, 0xE1, 0x0E, 0x00, 0x00, 0x00,0xF1, 0xE2, 0x12, 0x00, 0x00, 0x00, 0xF8, 0xF1, 0xE4, 0x0E,0x00, 0x00, 0x00, 0xF1, 0xE7, 0x12, 0x00, 0x00, 0x00, 0xF1,0xE1, 0x0F, 0x00, 0x00, 0x00, 0xF1, 0xE2, 0x11, 0x00, 0x00,0x00, 0xF8, 0xF1, 0xE4, 0x0F, 0x00, 0x00, 0x00, 0xF1, 0xE7,0x11, 0x00, 0x00, 0x00, 0xF4]for i in range(len(opcode)):match opcode[i]:case 0xF1:print(f"{i}", end=" ")k = i + 1match opcode[k]:case 0xE1:print("mov reg[0], flag[%d]" % opcode[i + 2])case 0xE2:print("mov reg[1], flag[%d]" % opcode[i + 2])case 0xE3:print("mov reg[2], flag[%d]" % opcode[i + 2])case 0xE4:print("mov flag[%d], reg[0]" % opcode[i + 2])case 0xE5:print("mov reg[3], flag[%d]" % opcode[i + 2])case 0xE7:print("mov flag[%d], reg[1]" % opcode[i + 2])i += 6case 0xF2:print(f"{i} xor reg[0], reg[1]")i += 1case 0xF5:print(f"{i} cmp 21")i += 1case 0xF4:print(f"{i} nop")i += 1case 0xF7:print(f"{i} mul reg[0], reg[3]")i += 1case 0xF8:print(f"{i} swap reg[0], reg[1]")i += 1case 0xF6:print(f"{i} reg[0] = reg[2] + reg[1]*2 + reg[0]*3")i += 1

输出结果:

汇编打印出来的前面一段是假的，分析后面的，

261 nop
288 cmp 21
289 mov reg[0], flag[0]
295 mov reg[1], flag[1]
301 xor reg[0], reg[1]
302 mov flag[0], reg[0]
308 mov reg[0], flag[1]
314 mov reg[1], flag[2]
320 xor reg[0], reg[1]
321 mov flag[1], reg[0]
327 mov reg[0], flag[2]
333 mov reg[1], flag[3]
339 xor reg[0], reg[1]
340 mov flag[2], reg[0]
346 mov reg[0], flag[3]
352 mov reg[1], flag[4]
358 xor reg[0], reg[1]
359 mov flag[3], reg[0]
365 mov reg[0], flag[4]
371 mov reg[1], flag[5]
377 xor reg[0], reg[1]
378 mov flag[4], reg[0]
384 mov reg[0], flag[5]
390 mov reg[1], flag[6]
396 xor reg[0], reg[1]
397 mov flag[5], reg[0]
403 mov reg[0], flag[6]
409 mov reg[1], flag[7]
415 mov reg[2], flag[8]
421 mov reg[3], flag[12]
427 reg[0] = reg[2] + reg[1]*2 + reg[0]*3
428 mul reg[0], reg[3]
429 mov flag[6], reg[0]
435 mov reg[0], flag[7]
441 mov reg[1], flag[8]
447 mov reg[2], flag[9]
453 mov reg[3], flag[12]
459 reg[0] = reg[2] + reg[1]*2 + reg[0]*3
460 mul reg[0], reg[3]
461 mov flag[7], reg[0]
467 mov reg[0], flag[8]
473 mov reg[1], flag[9]
479 mov reg[2], flag[10]
485 mov reg[3], flag[12]
491 reg[0] = reg[2] + reg[1]*2 + reg[0]*3
492 mul reg[0], reg[3]
493 mov flag[8], reg[0]
499 mov reg[0], flag[13]
505 mov reg[1], flag[19]
511 swap reg[0], reg[1]
512 mov flag[13], reg[0]
518 mov flag[19], reg[1]
524 mov reg[0], flag[14]
530 mov reg[1], flag[18]
536 swap reg[0], reg[1]
537 mov flag[14], reg[0]
543 mov flag[18], reg[1]
549 mov reg[0], flag[15]
555 mov reg[1], flag[17]
561 swap reg[0], reg[1]
562 mov flag[15], reg[0]
568 mov flag[17], reg[1]
574 nop

这里大致逻辑：
在这里插入图片描述

异或处理和数学运算，最后还有个交换。

编写exp

from z3 import *f1 = [0x69, 0x45, 0x2A, 0x37, 0x09, 0x17, 0xC5, 0x0B, 0x5C, 0x72,0x33, 0x76, 0x33, 0x21, 0x74, 0x31, 0x5F, 0x33, 0x73, 0x72]
f1[15], f1[17] = f1[17], f1[15]
f1[13], f1[19] = f1[19], f1[13]
f1[14], f1[18] = f1[18], f1[14]
s = Solver()
f = [BitVec(f"f{[i]}", 8) for i in range(13)]
s.add(f1[0] == f[0] ^ f[1])
s.add(f1[1] == f[1] ^ f[2])
s.add(f1[2] == f[2] ^ f[3])
s.add(f1[3] == f[3] ^ f[4])
s.add(f1[4] == f[4] ^ f[5])
s.add(f1[5] == f[5] ^ f[6])
s.add(f1[6] == (3 * f[6] + 2 * f[7] + f[8]) * f[12])
s.add(f1[7] == (3 * f[7] + 2 * f[8] + f[9]) * f[12])
s.add(f1[8] == (3 * f[8] + 2 * f[9] + f[10]) * f[12])
s.add(f1[9] == f[9])
s.add(f1[10] == f[10])
s.add(f1[11] == f[11])
s.add(f1[12] == f[12])
if s.check() == sat:t = s.model()for i in f:print(chr(t[i].as_long()), end='')print(bytes(f1[-7:]).decode())# Y0u_hav3_r3v3rs3_1t!