【CTF】Reverse Rust Vm 鹏城杯 逆向学习
浏览 260 | 评论 0 | 字数 8108
Xunflash
2022年07月07日
  • 前言

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

    分析

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

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

    image-20220707225656776

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

    image-20220707230312569

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

    image-20220707230530019

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

    image-20220707230611211

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

    image-20220707230658680

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

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

    image-20220707230920169

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

    img

    分析到这里其实基本逻辑已经差不多了,程序首先读取你的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

    本文作者:Xunflash
    本文链接:https://xunflash.top/index.php/archives/rustvm.html
    最后修改时间:2022-07-08 00:12:32
    本站未注明转载的文章均为原创,并采用 CC BY-NC-SA 4.0 授权协议,转载请注明来源,谢谢!
    评论
    114514
    textsms
    支持 Markdown 语法
    email
    link
    评论列表
    暂无评论