【CTF】Reverse Rust Vm 鹏城杯 逆向学习

前言

自己第一次做出来关于rust这方面的逆向题目，真的是体会到了什么叫做 💩 上加 💩

分析

首先拿到题目，题干就说是rustvm，关键这个题还就三百分..现在逆向真是太难了。

先定位到关键函数开始分析，上面的报错不用管，可以看到也是有一堆的东西

这边进去看一下可以知道这几个是干嘛的，配合动调可以知道把输入的东西转成int。这边有些thread线程的东西，含义不明也没关系，不影响接下来的做题，想搞懂这些都是干嘛的还是得动调一步一步走着看，这段代码重复了八次，每次都把

这边是一些输出的信息，这函数类似于printf，不用具体分析

这一块先malloc然后配合动调可以知道把输入的东西都读进去v129了

这一块是把vm的机器码写入，同样可以通过动调得知

下面的case操作，想都不用想，就是vm，这只能自己一个一个分析，配合动调可以拿到所有的机器码。这个真的是又臭又长，而且搭配着一堆_mm_loadu_这种函数，有的时候根本没法看反汇编的代码，我看的时候基本上都是对着汇编直接看的，去理解汇编每个寄存器在干嘛才是最折磨的事情。

这些操作里面有些很好分析，例如and，or，xor这些，但是有的真的不明白在干嘛，到做出来之后还是不懂他在干嘛..

翻到底下，可以看到一堆式子，虽然不知道这些_mm具体是用来干嘛的，但是基本上可以看得出来出题者想让你用z3解一下这一堆方程。实际上刚开始做这个题目也是想放弃，但是看到这一堆z3解出东西来了才想着继续做下去。

分析到这里其实基本逻辑已经差不多了，程序首先读取你的input，配合动调可以知道在一堆右移的时候把输入读进到v129（应该是模拟栈）上面，然后通过程序自带的opcode的一堆vm操作，最后通过一些式子进行验证操作，进行输出。

那么我们接下来就可以进行代码编写了。

代码

那首先先把最后一堆z3式子解出来，可以得到vm操作之后的密文。

from z3 import *
solver = Solver()
v127 = [BitVec("v127[%d]" % i,32) for i in range(16)]
solver.add(((v127[1] | v127[0] ^ 0xD4D1F400) == 0))
solver.add(((v127[3] | v127[2] ^ 0xD1417AE2) == 0))
solver.add(((v127[5] | v127[4] ^ 0xE743B46) == 0))
solver.add(((v127[7] | v127[6] ^ 0xD0C6E789) == 0))
      
solver.add(((v127[9] | v127[8] ^ 0xFB48126) == 0))
solver.add(((v127[11] | v127[10] ^ 0x838374C8) == 0))
solver.add(((v127[13] | v127[12] ^ 0x5220A3E1) == 0))
solver.add(((v127[15] | v127[14] ^ 0x8FC07772) == 0))

if solver.check() == sat:
        m = solver.model()
        for d in m.decls():
            print('%s == %s'% (d.name(),int(str(m[d]))))
'''输出
v127[4] == 242498374
v127[13] == 0
v127[0] == 3570529280
v127[8] == 263487782
v127[5] == 0
v127[14] == 2411755378
v127[1] == 0
v127[12] == 1377870817
v127[15] == 0
v127[3] == 0
v127[11] == 0
v127[2] == 3510729442
v127[9] == 0
v127[10] == 2206430408
v127[7] == 0
v127[6] == 3502696329
'''

然后是把case部分分析的东西，全部用python写出来，然后再动调dump出题目里面的opcode。（其实有三个操作我也没看懂，希望有大佬能解释下。）然后输出一段伪汇编代码。（自己能看懂就好了）

opcode=[0x0000000000000026, 0x0000000000000000, 0x0000000000000000, 0x0000000000000020, 0x0000000000000008, 0x0000000000000001, 0x0000000000000020, 0x0000000000000000, 0x0000000000000002, 0x0000000000000024, 0x0000000000000002, 0x0000000000000003, 0x0000000000000024, 0x0000000000000002, 0x0000000000000005, 0x0000000000000020, 0x0000000000000001, 0x0000000000000004, 0x0000000000000020, 0x000000000000000D, 0x0000000000000006, 0x0000000000000028, 0x0000000000000006, 0x0000000000000005, 0x0000000000000026, 0x0000000000000003, 0x0000000000000005, 0x000000000000002E, 0x0000000000000005, 0x0000000000000003, 0x0000000000000020, 0x0000000000000009, 0x0000000000000006, 0x0000000000000020, 0x0000000078F39600, 0x0000000000000007, 0x0000000000000027, 0x0000000000000006, 0x0000000000000005, 0x000000000000002C, 0x0000000000000007, 0x0000000000000005, 0x0000000000000026, 0x0000000000000003, 0x0000000000000005, 0x000000000000002E, 0x0000000000000005, 0x0000000000000003, 0x0000000000000020, 0x0000000000000011, 0x0000000000000006, 0x0000000000000020, 0x0000000085D40000, 0x0000000000000007, 0x0000000000000027, 0x0000000000000006, 0x0000000000000005, 0x000000000000002C, 0x0000000000000007, 0x0000000000000005, 0x0000000000000026, 0x0000000000000003, 0x0000000000000005, 0x000000000000002E, 0x0000000000000005, 0x0000000000000003, 0x0000000000000020, 0x0000000000000013, 0x0000000000000006, 0x0000000000000028, 0x0000000000000006, 0x0000000000000005, 0x0000000000000026, 0x0000000000000003, 0x0000000000000005, 0x0000000000000023, 0x0000000000000005, 0x0000000000000002, 0x0000000000000025, 0x0000000000000004, 0x0000000000000002, 0x0000000000000029, 0x0000000000000001, 0x0000000000000002, 0x000000000000002B, 0x0000000000000006, 0x0000000000000000]

for i in range(0,len(opcode),3):
    code=''
    if(opcode[i]==0x20):
        code+="mov "
        code+="*"+str(opcode[i+2])+' '
        code+=str(opcode[i+1])
    elif(opcode[i]==0x21):
        code+="mov "
        code+="*"+str(opcode[i+2])+' '
        code+=str(opcode[i+1])+'arg400'
    elif(opcode[i]==0x22):
        code+="mov "
        code+=str(opcode[i+2])+'arg400 '
        code+="*"+str(opcode[i+1])
    elif(opcode[i]==0x23):
        code+="mov "
        code+='**'+str(opcode[i+2])+' '
        code+="*"+str(opcode[i+1])
    elif(opcode[i]==0x24):
        code+="mov "
        code+='*'+str(opcode[i+2])+' '
        code+="*"+str(opcode[i+1])+'arg400'
    elif(opcode[i]==0x25):
        code+="add "
        code+='*'+str(opcode[i+2])+' '
        code+="*"+str(opcode[i+1])
    elif(opcode[i]==0x26):
        code+="xor "
        code+='*'+str(opcode[i+2])+' '
        code+="*"+str(opcode[i+1])
    elif(opcode[i]==0x27):
        code+="shl "
        code+='*'+str(opcode[i+2])+' '
        code+="*"+str(opcode[i+1])
    elif(opcode[i]==0x28):
        code+="shr "
        code+='*'+str(opcode[i+2])+' '
        code+="*"+str(opcode[i+1])
    elif(opcode[i]==0x29):
        code+="?1cmp0xffff "
        code+='*'+str(opcode[i+2])+' '
        code+="*"+str(opcode[i+1])
    elif(opcode[i]==0x2A):
        code+="?2mov "
        code+="arg3f8 "
        code+=str(opcode[i+1])
    elif(opcode[i]==0x2B):
        code+="?3mov "
        code+="arg3f8==0? "
        code+=str(opcode[i+1])
    elif(opcode[i]==0x2C):
        code+="and "
        code+='*'+str(opcode[i+2])+' '
        code+='*'+str(opcode[i+1])
    elif(opcode[i]==0x2D):
        code+="or "
        code+='*'+str(opcode[i+2])+' '
        code+='*'+str(opcode[i+1])
    elif(opcode[i]==0x2E):
        code+="mov "
        code+='*'+str(opcode[i+2])+' '
        code+='*'+str(opcode[i+1])
    else:
        print 'nop'
    print code
    
'''输出
xor *0 *0
mov *1 8
mov *2 0
mov *3 *2arg400
mov *5 *2arg400
mov *4 1
mov *6 13
shr *5 *6
xor *5 *3
mov *3 *5
mov *6 9
mov *7 2029229568
shl *5 *6
and *5 *7
xor *5 *3
mov *3 *5
mov *6 17
mov *7 2245263360
shl *5 *6
and *5 *7
xor *5 *3
mov *3 *5
mov *6 19
shr *5 *6
xor *5 *3
mov **2 *5
add *2 *4
?1cmp0xffff *2 *1
?3mov arg3f8==0? 6
'''

整理一下，给他写成python的代码（注意shr是逻辑右移），结合z3可以写成这样解出原始的输入（万物皆可z3）可以拿密文一个一个往下面这个z3里面带入，最后得到的东西拼接起来，就得到了flag。

from z3 import *
solver = Solver()
a5 = [BitVec("a5[%d]" % i,32) for i in range(2)]


solver.add(a5[1]==(((a5[0]^LShR(a5[0],13))^(2029229568&((a5[0]^LShR(a5[0],13))<<9)))^(2245263360&(((a5[0]^LShR(a5[0],13))^(2029229568&((a5[0]^LShR(a5[0],13))<<9)))<<17)))^LShR((((a5[0]^LShR(a5[0],13))^(2029229568&((a5[0]^LShR(a5[0],13))<<9)))^(2245263360&(((a5[0]^LShR(a5[0],13))^(2029229568&((a5[0]^LShR(a5[0],13))<<9)))<<17))),19))
solver.add(a5[1]==2411755378)

if solver.check() == sat:
        m = solver.model()
        for d in m.decls():
            print('%s == %s'% (d.name(),hex(int(str(m[d])))))

最后写个脚本输出flag

a=[0x39353333,0x38353563,0x63363339,0x39343630,0x66363161,0x62316533,0x33323234,0x62366339]
s=''
for i in a:
    s+=chr((i&0xff000000)>>24)+chr((i&0xff0000)>>16)+chr((i&0xff00)>>8)+chr((i&0xff))
print 'PCL{'+s+'}'
'''
PCL{9533855cc6399460f61ab1e33224b6c9}
'''

总结

这道题目感觉还是主要考察解题者的分析能力。分析rust和vm真的很折磨。我看有一位大佬在中午就解出来了，真的很离谱，不知道怎么做的。我陆陆续续看了一天，看到凌晨才分析出来。

不足

其实在分析vm的过程中，没有先输出一下opcode过滤一下可能不会出现的操作，减少分析的时间。我直接一股脑全看了。分析的时候也是反复来回看，心态也不好。说白了就是不熟练，缺乏那种看一遍稳过的自信。其他师傅要是能带带我就好了 😫

Xunflash 2022.07.07