从题目可知这是一道模拟虚拟机通过操作码对数据进行操作的题目，PE64无壳，放入ida，对函数进行分析
在vm_init中创建结构体得到
其中reg0-3是4个寄存器，g_action是操作码的集合，vm_main是vm根据对应操作码对reg和输入数据的操作，xor，input，add_ip，swpa，add_mul都是对寄存器的操作
在vm_start函数中，当读到操作码不为F4时进入函数
for ( i = 0; *a1->g != *(&a1->opcode1 + 16 * i); ++i ) 在遍历g_action是否有操作码满足上述init函数中的操作码，如果有则调用对应操作码的函数，我们就可以写脚本来查看所有操作
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 x in range(len(opcode)):
code=opcode[x]
#print(hex(opcode[x]))
if opcode[x]==0xF4:
print("\n")
if opcode[x]==0xF5:
print("input:__________________________21")
if opcode[x]==0xF2:
print("r0=r0 ^ r1")
if opcode[x]==0xF7:
print("r0=r0 * r4")
if opcode[x]==0xF8:
print("swap(r0,r4)")
if opcode[x]==0xF6:
print("r0=2 * r1 + r2 + 3 * r0")
if opcode[x]==0xF1:
fun_op=opcode[x+1]
num=opcode[x+2]
if fun_op == 0xE1:
r0 = num
print(f"r0=input[{num}]")
if fun_op == 0xE2:
r1 = num
print(f"r1=input[{num}]")
if fun_op == 0xE3:
r2 = num
print(f"r2=input[{num}]")
if fun_op == 0xE4:
print(f"input[{num}]=r0")
if fun_op == 0xE5:
r3 = num
print(f"r4=input[{num}]")
if fun_op == 0xE7:
print(f"input[{num}]=r1")#输出
input:__________________________21
r0=input[0]
r0=r0 ^ r1
input[32]=r0
r0=input[1]
r0=r0 ^ r1
input[33]=r0
r0=input[2]
r0=r0 ^ r1
input[34]=r0
r0=input[3]
r0=r0 ^ r1
input[35]=r0
r0=input[4]
r0=r0 ^ r1
input[36]=r0
r0=input[5]
r0=r0 ^ r1
input[37]=r0
r0=input[6]
r0=r0 ^ r1
input[38]=r0
r0=input[7]
r0=r0 ^ r1
input[39]=r0
r0=input[8]
r0=r0 ^ r1
input[40]=r0
r0=input[9]
r0=r0 ^ r1
input[41]=r0
r0=input[10]
r0=r0 ^ r1
input[42]=r0
r0=input[11]
r0=r0 ^ r1
input[43]=r0
r0=input[12]
r0=r0 ^ r1
input[44]=r0
r0=input[13]
r0=r0 ^ r1
input[45]=r0
r0=input[14]
r0=r0 ^ r1
input[46]=r0
r0=input[15]
r0=r0 ^ r1
input[47]=r0
r0=input[16]
r0=r0 ^ r1
input[48]=r0
r0=input[17]
r0=r0 ^ r1
input[49]=r0
r0=input[18]
r0=r0 ^ r1
input[50]=r0
r0=input[19]
r0=r0 ^ r1
input[51]=r0
input:__________________________21
r0=input[0]
r1=input[1]
r0=r0 ^ r1
input[0]=r0
r0=input[1]
r1=input[2]
r0=r0 ^ r1
input[1]=r0
r0=input[2]
r1=input[3]
r0=r0 ^ r1
input[2]=r0
r0=input[3]
r1=input[4]
r0=r0 ^ r1
input[3]=r0
r0=input[4]
r1=input[5]
r0=r0 ^ r1
input[4]=r0
r0=input[5]
r1=input[6]
r0=r0 ^ r1
input[5]=r0
r0=input[6]
r1=input[7]
r2=input[8]
r4=input[12]
r0=2 * r1 + r2 + 3 * r0
r0=r0 * r4
input[6]=r0
r0=input[7]
r1=input[8]
r2=input[9]
r4=input[12]
r0=2 * r1 + r2 + 3 * r0
r0=r0 * r4
input[7]=r0
r0=input[8]
r1=input[9]
r2=input[10]
r4=input[12]
r0=2 * r1 + r2 + 3 * r0
r0=r0 * r4
input[8]=r0
r0=input[13]
r1=input[19]
swap(r0,r4)
input[13]=r0
input[19]=r1
r0=input[14]
r1=input[18]
swap(r0,r4)
input[14]=r0
input[18]=r1
r0=input[15]
r1=input[17]
swap(r0,r4)
input[15]=r0
input[17]=r1该操作分为两部分，但第一部分为假的flag故flag应在第二段，写z3脚本爆破得到
def swap(a, b):
a, b = b, a
return a, b
flag = [105, 69, 42, 55, 9, 23, 197, 11, 92, 114,
51, 118, 51, 33, 116, 49, 95, 51, 115, 114]
flag[15], flag[17] = swap(flag[15], flag[17])
flag[14], flag[18] = swap(flag[14], flag[18])
flag[19], flag[13] = swap(flag[19], flag[13])
r=[BitVec(f"r{i}",8) for i in range(20)]
s=Solver()
s.add(r[9]==flag[9])
s.add(r[10]==flag[10])
s.add(r[11]==flag[11])
s.add(r[12]==flag[12])
s.add(r[13]==flag[13])
s.add(r[14]==flag[14])
s.add(r[15]==flag[15])
s.add(r[16]==flag[16])
s.add(r[17]==flag[17])
s.add(r[18]==flag[18])
s.add(r[19]==flag[19])
s.add(r[0]^r[1]==(flag[0]))
s.add(r[0]^r[1]==(flag[0]))
s.add(r[1]^r[2]==(flag[1]))
s.add(r[2]^r[3]==(flag[2]))
s.add(r[3]^r[4]==(flag[3]))
s.add(r[4]^r[5]==(flag[4]))
s.add(r[5]^r[6]==(flag[5]))
s.add(((flag[10]) +2 * (flag[9]) + 3 * r[8])*(flag[12])==(flag[8]))
s.add(((flag[9]) +2 * r[8] + 3 * r[7])*(flag[12])==(flag[7]))
s.add((r[8] +2 * r[7] + 3 * r[6])*(flag[12])==(flag[6]))
if s.check()==sat:
ans=s.model()
print(ans)
for x in r:
print(chr(ans[x].as_long()),end="")
Comments NOTHING