HCTF逆向题目详析

前言

很有水平的一场比赛，RE的几道题目质量都非常高。

由于自己的原因，只是看了题，没做，感觉就算认真做，也做不出来几题，毕竟太菜。哈哈！

下面就先从最简单的开始写！

seven

简单的签到题，只不过是放在了windows驱动里，从没接触过，稍微带来了一点麻烦，算法是很经典的吃豆子游戏，刚好看加解密时看到了，在键盘扫描码卡了很久。

关于驱动开发的一些API可以在 MDSN 上找到相关说明

如DriverEntry函数就是一个驱动程序的入口函数，过多的我就不班门弄斧了。

总之这个题就是有不认识的API，就直接在MDSN上找函数说明即可。

关于解题，还是搜索字符串，找到The input is the flag字样，交叉引用到sub_1400012F0函数，如果看过加解密的同学，应该能一眼看出这是吃豆子游戏（这可不是打广告），细看还真是！

就是如下这个矩阵

从o开始，沿着.走，一直走到7即可。

0x11 表示向上

0x1f 表示向下

0x1e 表示向左

0x20 表示向右

当时一直在想0x11和输入的关系，最后才知道原来是键盘的扫描码，分别对应wasd

OK那么此题轻易的解决了！我是不是很水！

（下面几题都算是复现，我是一个没有感情的杀手！)

LuckyStar

别看程序这么大只不是VS静态编译了而已。

其实也不难，一进来先搜索字符串，看到idaq.exe，x32dbg等常见调试器的字样，很明显有反调试，并且还看到一大段未识别的数据，感觉很像是自解码的部分，其实真正的加密部分就在这里。

关于反调试，不必紧张，动态调试时手动修改下寄存器即可。通过交叉引用找到TlsCallback_0函数，判断之前下断，绕过即可（直接patch比较方便）。

之后便是程序的自解密部分，最后便可以看到真正的加密的过程。

将00401780至00401939 undefine一下然后重新create function，IDA便可以识别，接下来的一段解密也是类似的，最后进行一个比较。有一点需要注意，在动调时候不知道什么情况，程序就蹦了，需要手动在401780函数处set ip然后跳转过去

加密部分其实就是变形的base64加上一个异或，类似的题目做的太多了，解密脚本如下：

table='''abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789+/'''
def mydecodeb64(enc):
    enc=enc.replace("=","")
    x="".join(map(lambda x:bin(table.index(x))[2:].zfill(6),enc))
    # print x
    for ap in range(8-(len(x)%8)):
        x+='0'
    # print x
    plain=[]
    for i in range((len(x))/8):
        plain.append(chr(eval('0b'+x[i*8:(i+1)*8])))
    return "".join(plain).replace("x00","")
def myencodeb64(plain):
    en=[]
    encode=[]
    for d in list(plain):
        en.append(bin(ord(d))[2:].zfill(8))
    plain="".join(en)
    for ap in range(6-(len(plain)%6)):
        plain+='0'
    # print enc
    for i in range((len(plain))/6):
        encode.append(table[eval('0b'+plain[i*6:(i+1)*6])])
    return "".join(encode)
in_base='D3D3D3D3D3D3D3D3D3D3D3D3D3D3D3D3'
enc=[0x49, 0xE6, 0x57, 0xBD, 0x3A, 0x47, 0x11, 0x4C, 0x95, 0xBC, 0xEE, 0x32, 0x72, 0xA0, 0xF0, 0xDE, 0xAC, 0xF2, 0x83, 0x56, 0x83, 0x49, 0x6E, 0xA9, 0xA6, 0xC5, 0x67, 0x3C, 0xCA, 0xC8, 0xCC, 0x05]
rand=[0x4c,0xb2,0x7d,0xbe,0x04,0x3a,0x06,0x27,0x94,0xc1,0xdc,0x55,0x77,0xe5,0x8d,0x81,0x85,0xa6,0xf2,0x2d,0x83,0x1e,0x58,0xdc,0x96,0x81,0x1b,0x55,0xc8,0x8a,0xb5,0x0b]
f=[]
for i in range(32):
    f.append(chr(rand[i]^enc[i]^ord(in_base[i])))
a = "".join(f)
print a
flag=mydecodeb64(a)
print flag

PolishDuck

比赛的时候就简单看了一眼，只知道是个arduino程序。

这题可以参考 文章

对于hex文件，先使用hex2bin进行转化 在此下载

通过strings可知为Arduino Leonardo板子。

同样的为atmega32u4 在此 可以得到对应板子的IDA配置信息，此时再次载入bin文件，IDA如下配置。

既然后notepad.exe字样，那么就从这里开始分析，其实这里想到了badusb，正好我之前在大二的时候玩过这玩意，这时居然能派上用场.

使用Arduino编写一个简单的HID例程，设置如下：

代码如下：

#include <Keyboard.h>

void setup() {
  // put your setup code here, to run once:
  Keyboard.begin();
  delay(5000);
  Keyboard.press(KEY_LEFT_GUI);
  delay(500);
  Keyboard.press('r');
  delay(500);
  Keyboard.release(KEY_LEFT_GUI);
  Keyboard.release('r');
  Keyboard.press(KEY_CAPS_LOCK);
  Keyboard.release(KEY_CAPS_LOCK);
  delay(500);
  Keyboard.println("NOTEPAD.EXE");
  delay(800);
  Keyboard.println();
  delay(800);


}

void loop() {
  // put your main code here, to run repeatedly:

}

并且导出编译后的二进制文件

此时会在目录下出现两个hex文件,其中bootloader是我们需要关注的，同样的使用hex2bin转化，丢入IDA进行查看。

OK，很明显，和题目的结构基本上一致，所以进行类比法即可。

我们关注到sub_9B5函数，前面一段无非是进行初始化操作

根据 Keyboard.h 可以知道按键所对应的机器码，同时看网上一些文章可以知道println读取的数据是从RAM中获得，而__RESET函数中包含了初始化RAM的工作，结合着源代码，可以得到以下过程：

回到题目中来，也是类似的,这里需要确定println函数输出的偏移，在hex窗口确定数据范围，然后手动取得offset，通过 python 将每一个输出得到，最后eval计算即可。

notepad.exe 对应 0x140
44646        对应 0x14c
遇到'x00'结束
注意一点hex中显示的和实际的是不同的！！！
因为println的参数中只确定了起始偏移，结束需要根据‘x00'来判断。
所以有的符号会有重复！
否则这题就太简单了！！！

脚本如下：

from libnum import n2s,s2n
a=open("PolishDuck2.bin",'rb').read()
data=a[0x1a9c:0x1e3e]
offset=[0x14C ,0x153 ,0x162 ,0x177 ,0x18B,0x1A9,0x1C8,0x1D3,0x1EB,0x1FE,0x25E ,0x207,0x21C,0x227 ,0x246 ,0x261 ,0x270 ,0x28B,0x298,0x2A3,0x2B1,0x25C ,0x2BA,0x2C5,0x2D0,0x2D7,0x2F2,0x307,0x310,0x25E ,0x327 ,0x346 ,0x3DC,0x34D ,0x364 ,0x373 ,0x38F,0x3A6,0x3B3,0x3BF,0x3D0,0x3DF,0x3EF,0x400,0x44B ,0x413,0x42C ,0x43B ,0x44F ,0x452 ,0x490,0x45F ,0x46C ,0x47D ,0x48E,0x497,0x49E,0x4B5,0x4CB,0x445 ,0x445 ,0x4D6,0x44D ,0x44D ,0x494,0x4E5,0x44f]
flag=''
for i in range(len(offset)):
    start = offset[i]-0x14c
    end = start+1
    index = start
    while end<len(data):
        if data[end] == 'x00':
            break
        end+=1
    flag+=data[start:end]

print n2s(eval(flag))

Spiral

此次比赛中难度最大的题目，既涉及到用户层，又涉及到内核驱动层，我会详细的写。

程序的结构还是比较分明的，先是第一部分。

checkgateone

首先会检查系统版本号，这里观察一下本地版本号的值，直接patch即可，图中我已经patch。

随后校验输入是否为hctf{***}其中要求***长度为0x49

之后分割输入的字符串input[:46]&input[-27:]

随后将前一部分进行一个较为复杂的校验。过程简述如下：

首先通过a1[i] & 7;和(a1[i] & 0x78) >> 3;获取opcode

之后进入另一个函数，经过一个类似vm的过程得到data

并将op和data进行拼接

最后将拼接的数组同固定数组比较。

OK！我想第一部分对大多数人来说还是比较简单的，接下来我们便可以解出前半段flag。脚本如下：

def gate_one():
    static_data=[0x07, 0xE7, 0x07, 0xE4, 0x01, 0x19, 0x03, 0x50, 0x07, 0xE4, 0x01, 0x20, 0x06, 0xB7, 0x07, 0xE4, 0x01, 0x22, 0x00, 0x28, 0x00, 0x2A, 0x02, 0x54, 0x07, 0xE4, 0x01, 0x1F, 0x02, 0x50, 0x05, 0xF2, 0x04, 0xCC, 0x07, 0xE4, 0x00, 0x28, 0x06, 0xB3, 0x05, 0xF8, 0x07, 0xE4, 0x00, 0x28, 0x06, 0xB2, 0x07, 0xE4, 0x04, 0xC0, 0x00, 0x2F, 0x05, 0xF8, 0x07, 0xE4, 0x04, 0xC0, 0x00, 0x28, 0x05, 0xF0, 0x07, 0xE3, 0x00, 0x2B, 0x04, 0xC4, 0x05, 0xF6, 0x03, 0x4C, 0x04, 0xC0, 0x07, 0xE4, 0x05, 0xF6, 0x06, 0xB3, 0x01, 0x19, 0x07, 0xE3, 0x05, 0xF7, 0x01, 0x1F, 0x07, 0xE4]
    s=''
    for i in range(0, len(static_data), 2):
        op = static_data[i]
        op_data = static_data[i+1]
        if op == 0:
            op_data-=34
        if op == 1:
            op_data-=19
        if op == 2:
            op_data-=70
        if op == 3:
            op_data-=66
        if op == 4:
            op_data^=0xca
        if op == 5:
            op_data^=0xfe
        if op == 6:
            op_data^=0xbe
        if op == 7:
            op_data^=0xef
        s+=chr(op|((op_data<<3)&0x78))
    print s

随后我们构造输入hctf{G_1s_iN_y0 @r_aRe4_0n5_0f_Th5_T0ugHtEST_En1gMa_aaaaaaaaaaaaaaaaaaaaaaaaaaa }进入第二阶段

checkgatetwo

首先通过DriverEntry入口函数，进行查看，有过seven那题的了解，可以知道前面的操作都是在进行注册驱动，不影响解体，而且也不是重点内容。

唯一可疑的函数就是sub_403310.

随便选几个函数进行查看，发现从未见过的指令。如sub_401440函数中的CPUID指令。

CPUID操作码是一个面向x86架构的处理器补充指令

通过使用CPUID操作码，软件可以确定处理器的类型和特性支持（例如MMX/SSE）

继续向下查看

readcr0指令

Reads the CR0 register and returns its value.  This intrinsic is only available in kernel mode, and the routine is only available as an intrinsic.

貌似是读取了rc0寄存器，并且必须内核态。丧气脸！

rdmsr指令

Reads the contents of a 64-bit model specific register (MSR) specified in the ECX register into registers EDX:EAX

writecr4指令就是向rc4寄存器写入

getcallerseflags指令

Returns the EFLAGS value from the caller’s context.

以上指令的解释都可以通过msdn搜索

vmxon指令

这个指令是vmx指令集中的一个，意味着开始硬件虚拟化，并且在开启硬件虚拟化之前程序会检查rc0和rc4寄存器以及CPU是否支持等条件，这也就是在之前看到的那些代码的作用

我之前在看加解密时看到过VT技术，不过太菜没看懂，趁着这个机会好好学习一下，下文关于指令部分大多参考自网上资料。

invd指令片上的高速缓存无效。

继续往下查看，发现在sub_401682函数中做了大量的操作，猜测应该是在进行vmx的初始化操作。

关于vmx指令， 参考链接 。

关于vmm简介， 参考链接

关于进入vmx的过程， 参考链接

以上三篇文章请一定要仔细阅读！

sub_4015AF函数中vmptrld指令加载一个VMCS结构体指针作为当前操作对象

sgdt/sidt指令存储全局/中断描述符表格寄存器 参考链接

之后的过程可以参考第三篇文章，过程一致，先初始化VMCS region，装载VMCS region，设置VMCS region中的相关域

其中分别设置了Guest的的region和HOST的region

那么0x401738地址所对应的函数便是VMExitProc函数也就是VMM的程序入口地址。这里IDA并没有将其识别出来，所以手动创建函数

（询问了一下v爷爷，需要将最后的3个0xcc NOP掉就可以正常创建函数）

首先我们要说明的是sub_401631函数中的vmlaunch指令，驱动程序使用vmlaunch启动Guest虚拟机，执行一条指令（导致vmexit），然后返回主机。

VMExitProc函数用来接受Guest VM的特殊消息，从而进行执行，这也就是为什么choose_func函数没有找到交叉引用的原因！

我们可以参考这篇 文章

从而可以知道一些特殊指令，如下：

#defineEXIT_REASON_CPUID               10
#defineEXIT_REASON_INVD                13
#defineEXIT_REASON_VMCALL              18 
#defineEXIT_REASON_CR_ACCESS            28 
#defineEXIT_REASON_MSR_READ            31
#defineEXIT_REASON_MSR_WRITE           32

以上图片来自上面的博客

ok，继续往下，刚刚程序执行了vmlaunch之后，便会启动Guest Vm,然后会执行如下代码：

首先EAX=0xDEADBEEF，触发cpuid和invd指令之后EAX=0x174

触发rdmsr指令，然后便会来到vmcalls函数,注意下这里都是通过EAX寄存器传参

其中rdmsr函数对应msr_read_func函数，invd对应invd_func函数,vmcall对应vmcall_func函数，我已将函数重命名:XD

需要注意的是在Guest VM未启动之前，执行cpuid等指令时并不会触发VMExitProc函数

所以之后便是在Guest VM和VMM之间通过vmresume和触发指令不断的进行切换执行，最终的加密逻辑便在Guest VM中

接下来大致说明一下事件处理函数的作用。

cpuid_func对op进行解码，并初始化数独

invd_func对op进行乱序操作

vmcall_func解析op，主要就是这三个函数。

（！惊了，写到这里的时候电脑突然烧了！烧了！伤脑筋啊，最近一直有事，所以WP不得不推迟写了。见谅见谅！原谅绿～）

所以VMM的执行过程：

sub_401596函数vmxon打开vmx的开关。

sub_401690函数初始化Guest VM，并为Guest VM注册相应的入口函数，最后通过vmlaunch运行Guest VM，此时会对9*9的矩阵进行初始化，然后通过vmcalls函数进行加密变换。

vmcalls的处理流程如下：

rdmsr(0x176);对应

else if ( switch_code == 0x176 )
  {
    v3 = dword_405160;
    result = dword_4050C0[0];
    v4 = dword_4050C0[0];
    for ( k = 8; k; --k )
    {
      result = 9 * k;
      dword_405040[9 * k] = dword_405040[9 * (k - 1)];
    }
    dword_405040[0] = v3;
    for ( l = 0; l < 8; ++l )
    {
      dword_4050C0[l] = dword_4050C4[l];
      result = l + 1;
    }
    dword_4050E0 = v4;
  }

简单的移位变换。

invd对应三种变换方式（略）

vmcall根据op的不同进行相应的运算。

以vmcall(0x30133403);为例进行一个说明：

v1`为op的第一个字节即0x30，用来判断进行何种操作  
`i`为数据在矩阵中的坐标(x,y)，0x13即代表(1,3)  
`0x34`为第三个字节，用来判断是否倒序  
`0x03`表示`input`的位置

当我们在判断每个字节的作用时，注意变量的类型。

其实从本质上来讲就是根据我们的输入产生一张数独表，并进行校验是否满足数独的要求。所以解体思路上来讲我们需要先解出最后的数独，然后恢复出input。

这里通常使用z3求解器进行求解，所以我们设置好变量类型照着程序走一遍流程就好了，从IDA中抠出代码，然后进行适当修复，说的好像很简单，其实做起来并不是很轻松。

接下来我就写一遍过程：

在vmlunch指令之后会开始响应ExitReason，首先便是cpuid指令，进入choose_func函数，由于是第一次执行，因此会进行初始化执行init_box函数（已重命名），如下：

通常我是用python来编写脚本，在修改之前，我们需要弄清两个数据结构，一个是9*9的数独即data[9][9],另一个是op[10]。判断方法如下：

data[9][9]从init_box函数中可以较为明显的看出dword_405030；

op[10]在vmcall_func中如下

从dword_405378往后的10个数据均在vmcall_func函数中有交叉引用

了解到这些之后，我们继续进行修复。

如下代码：

def init_box():
    result = data[40]
    v6 = data[40]
    for i in range(4):
        data[8*i+40]=data[8*i+40-1]
        for j in range(2*i+1):
            data[3 - i + 9 * (i + 4 - j)]=data[3 - i + 9 * (i + 4 - (j + 1))]
        for k in range(2 * i + 2):
            data[k + 9 * (3 - i) + 3 - i] = data[10 * (3 - i) + k + 1]
        for l in range(2 * i + 2):
            data[9 * (l + 3 - i) + i + 5] = data[9 * (3 - i + l + 1) + i + 5]
        m=0
        while m < result:
            result = 2*i+2
            data[9 * (i + 5) + i + 5 - m] = data[9 * (i + 5) + i + 5 - (m + 1)]
            m+=1
    data[72]=v6

然后会进入cpuid_func

类似的，代码如下：

def cpuid_func(switch_code):
    if switch_code == 0xDEADBEEF:
        for i in range(10):
            op[i]^=key1[i]
    elif switch_code == 0xCAFEBABE:
        for j in range(10):
            op[j]^=key2[j]

接下来恢复invd_func：

def invd_func(switch_code):
    if switch_code == 0x4433:
        for i in range(5):
            v0 = op[2*i]
            op[2*i]=op[2*i+1]
            op[2*i+1]=v0
    elif switch_code == 0x4434:
        v5 = op[0]
        for j in range(9):
            op[j]=op[j+1]
        op[9]=v5
    elif switch_code == 0x4437:
        v3 = op[7]
        for k in range(3):
            op[k+7]=op[7-k-1]
            if k == 2:
                op[7-k-1]=op[3]
            else:
                op[7-k-1]=op[k+7+1]
        for l in range(1):
            op[3]=op[3-l-2]
            op[3-l-2]=op[3-l-1]
        op[3-1-1]=v3

接下来便会进入vmcalls函数进行一系列变换，最后我们恢复出rdmsr和vmcall函数

dword_405170的转换过程可以如下计算：

def rdmsr(switch_code):
    if switch_code == 0x174:
        v6=data[80]
        v7=data[8]
        for i in range(8,0,-1):
            data[10*i]=data[9*(i-1)+i-1]
        data[0]=v6
        for j in range(1,9):
            data[8*j]=data[8*j+8]
        data[8*9]=v7            # Look at me!!!
    if switch_code == 0x176:
        v3 = data[76]
        result = data[36]
        v4 = data[36]
        for k in range(8,0,-1):
            result = 9*k
            data[9*k+4]=data[9*(k-1)+4]
        data[4]=v3
        for l in range(8):
            data[l+36]=data[l+37]
            result=l+1
        data[44]=v4

其中在rdmsr遇到了一个坑

dword_405030[8 * j] = v7;此时j应该为9，而在使用python的for语句时data[8*j]=v7此时的j为8，这也就直接导致，我调试了好久.23333

def vmcall_func(switch_code):
    v1 = (switch_code >> 24)
    i = ((switch_code>>16)&0xf)+9*((((switch_code>>16)&0xff)>>4)&0xf)
    byte_switch_code = switch_code&0xff
    if ((switch_code>>8)&0xff == 0xcc):
        d_input = m_input
    else:
        d_input = m_input[::-1]

    if v1 == op[0]:
        data[i]=d_input[byte_switch_code]
    elif v1 == op[1]:
        data[i]+=d_input[byte_switch_code]
        data[i]&=0xff
    elif v1 == op[2]:
        data[i]-=d_input[byte_switch_code]
        data[i]&=0xff
    elif v1 == op[3]:
        data[i]=data[i]/d_input[byte_switch_code]
        data[i]&=0xFF
    elif v1 == op[4]:
        data[i]*=d_input[byte_switch_code]
        data[i]&=0xFF
    elif v1 == op[5]:
        data[i]^=d_input[byte_switch_code]
        data[i]&=0xFF
    elif v1 == op[6]:
        data[i]^=d_input[byte_switch_code-1]+d_input[byte_switch_code]-d_input[byte_switch_code+1]
        data[i]&=0xFF
    elif v1 == op[7]:
        data[i]^=d_input[byte_switch_code]*16
        data[i]&=0xFF
    elif v1 == op[8]:
        data[i]|=d_input[byte_switch_code]
        data[i]&=0xFF
    elif v1 == op[9]:
        data[i]^=d_input[byte_switch_code+1]^d_input[byte_switch_code-1]^(d_input[byte_switch_code-2]+d_input[byte_switch_code]-d_input[byte_switch_code+2])
        data[i]&=0xFF
    elif v1 == 0xDD:
        print "vmx_off"
    elif v1 == 0xFF:
        check()
        return
    else:
        print "error"

注意操作符的运算顺序，python在带来便利的同时，也会为我们带来困扰。

最后会进行check函数，据出题人证实确实是代码写错了，但是并不影响我们解题。check的过程其实就是对数独进行校验的过程，基于此我们进行恢复。

off_405534是check_data的指针

def check():
    for n in range(9):
        v5=[0 for m in range(9)]
        for i in range(9):
            v5[i]=data[((check_data[n]+i)&0xF)+9 * (((check_data[n]+i) >> 4) & 0xF)]
            s.add(v5[i]>0,v5[i]<10)
        for j in range(8):
            for k in range(j+1,9):
                s.add(v5[j]!=v5[k])

这里使用z3求解器，添加了约束条件。接下来将z3求解的相应代码补全。相关的数据可以通过lazyida插件进行导出。最终完整代码如下：

def gate_one():
    static_data=[0x07, 0xE7, 0x07, 0xE4, 0x01, 0x19, 0x03, 0x50, 0x07, 0xE4, 0x01, 0x20, 0x06, 0xB7, 0x07, 0xE4, 0x01, 0x22, 0x00, 0x28, 0x00, 0x2A, 0x02, 0x54, 0x07, 0xE4, 0x01, 0x1F, 0x02, 0x50, 0x05, 0xF2, 0x04, 0xCC, 0x07, 0xE4, 0x00, 0x28, 0x06, 0xB3, 0x05, 0xF8, 0x07, 0xE4, 0x00, 0x28, 0x06, 0xB2, 0x07, 0xE4, 0x04, 0xC0, 0x00, 0x2F, 0x05, 0xF8, 0x07, 0xE4, 0x04, 0xC0, 0x00, 0x28, 0x05, 0xF0, 0x07, 0xE3, 0x00, 0x2B, 0x04, 0xC4, 0x05, 0xF6, 0x03, 0x4C, 0x04, 0xC0, 0x07, 0xE4, 0x05, 0xF6, 0x06, 0xB3, 0x01, 0x19, 0x07, 0xE3, 0x05, 0xF7, 0x01, 0x1F, 0x07, 0xE4]
    s=''
    for i in range(0, len(static_data), 2):
        op = static_data[i]
        op_data = static_data[i+1]
        if op == 0:
            op_data-=34
        if op == 1:
            op_data-=19
        if op == 2:
            op_data-=70
        if op == 3:
            op_data-=66
        if op == 4:
            op_data^=0xca
        if op == 5:
            op_data^=0xfe
        if op == 6:
            op_data^=0xbe
        if op == 7:
            op_data^=0xef
        s+=chr(op|((op_data<<3)&0x78))
    print s

def init_box():
    result = data[40]
    v6 = data[40]
    for i in range(4):
        data[8*i+40]=data[8*i+40-1]
        for j in range(2*i+1):
            data[3 - i + 9 * (i + 4 - j)]=data[3 - i + 9 * (i + 4 - (j + 1))]
        for k in range(2 * i + 2):
            data[k + 9 * (3 - i) + 3 - i] = data[10 * (3 - i) + k + 1]
        for l in range(2 * i + 2):
            data[9 * (l + 3 - i) + i + 5] = data[9 * (3 - i + l + 1) + i + 5]
        m=0
        while m < result:
            result = 2*i+2
            data[9 * (i + 5) + i + 5 - m] = data[9 * (i + 5) + i + 5 - (m + 1)]
            m+=1
    data[72]=v6

def cpuid_func(switch_code):
    if switch_code == 0xDEADBEEF:
        for i in range(10):
            op[i]^=key1[i]
    elif switch_code == 0xCAFEBABE:
        for j in range(10):
            op[j]^=key2[j]

def invd_func(switch_code):
    if switch_code == 0x4433:
        for i in range(5):
            v0 = op[2*i]
            op[2*i]=op[2*i+1]
            op[2*i+1]=v0
    elif switch_code == 0x4434:
        v5 = op[0]
        for j in range(9):
            op[j]=op[j+1]
        op[9]=v5
    elif switch_code == 0x4437:
        v3 = op[7]
        for k in range(3):
            op[k+7]=op[7-k-1]
            if k == 2:
                op[7-k-1]=op[3]
            else:
                op[7-k-1]=op[k+7+1]
        for l in range(1):
            op[3]=op[3-l-2]
            op[3-l-2]=op[3-l-1]
        op[3-1-1]=v3

def rdmsr(switch_code):
    if switch_code == 0x174:
        v6=data[80]
        v7=data[8]
        for i in range(8,0,-1):
            data[10*i]=data[9*(i-1)+i-1]
        data[0]=v6
        for j in range(1,9):
            data[8*j]=data[8*j+8]
        data[8*9]=v7            # Look at me!!!
    if switch_code == 0x176:
        v3 = data[76]
        result = data[36]
        v4 = data[36]
        for k in range(8,0,-1):
            result = 9*k
            data[9*k+4]=data[9*(k-1)+4]
        data[4]=v3
        for l in range(8):
            data[l+36]=data[l+37]
            result=l+1
        data[44]=v4

def check():
    for n in range(9):
        v5=[0 for m in range(9)]
        for i in range(9):
            v5[i]=data[((check_data[9*n+i])&0xF)+9 * ((((check_data[9*n+i])) >> 4) & 0xF)]
            s.add(v5[i]>0,v5[i]<10)
        for j in range(9):
            for k in range(j+1,9):
                s.add(v5[j]!=v5[k])

def vmcall_func(switch_code):
    v1 = (switch_code >> 24)
    i = ((switch_code>>16)&0xf)+9*((((switch_code>>16)&0xff)>>4)&0xf)
    byte_switch_code = switch_code&0xff
    if ((switch_code>>8)&0xff == 0xcc):
        d_input = m_input
    else:
        d_input = m_input[::-1]

    if v1 == op[0]:
        data[i]=d_input[byte_switch_code]
    elif v1 == op[1]:
        data[i]+=d_input[byte_switch_code]
        data[i]&=0xff
    elif v1 == op[2]:
        data[i]-=d_input[byte_switch_code]
        data[i]&=0xff
    elif v1 == op[3]:
        data[i]=data[i]/d_input[byte_switch_code]
        data[i]&=0xFF
    elif v1 == op[4]:
        data[i]*=d_input[byte_switch_code]
        data[i]&=0xFF
    elif v1 == op[5]:
        data[i]^=d_input[byte_switch_code]
        data[i]&=0xFF
    elif v1 == op[6]:
        data[i]^=d_input[byte_switch_code-1]+d_input[byte_switch_code]-d_input[byte_switch_code+1]
        data[i]&=0xFF
    elif v1 == op[7]:
        data[i]^=d_input[byte_switch_code]*16
        data[i]&=0xFF
    elif v1 == op[8]:
        data[i]|=d_input[byte_switch_code]
        data[i]&=0xFF
    elif v1 == op[9]:
        data[i]^=d_input[byte_switch_code+1]^d_input[byte_switch_code-1]^(d_input[byte_switch_code-2]+d_input[byte_switch_code]-d_input[byte_switch_code+2])
        data[i]&=0xFF
    elif v1 == 0xDD:
        print "vmx_off"
    elif v1 == 0xFF:
        check()
        return
    else:
        print "error"

from z3 import *
s=Solver()
m_input = [BitVec("fla%d"%i,32) for i in range(27)]
for i in m_input:
    s.add(i>32,i<127)

op=[0xA3,0xF9,0x77,0xA6,0xC1,0xC7,0x4E,0xD1,0x51,0xFF]
key1=[0x00000090, 0x000000CD, 0x00000040, 0x00000096, 0x000000F0, 0x000000FE, 0x00000078, 0x000000E3, 0x00000064, 0x000000C7]
key2=[0x00000093, 0x000000C8, 0x00000045, 0x00000095, 0x000000F5, 0x000000F2, 0x00000078, 0x000000E6, 0x00000069, 0x000000C6]
data=[0x00000007, 0x000000CE, 0x00000059, 0x00000023, 0x00000009, 0x00000005, 0x00000003, 0x00000001, 0x00000006, 0x00000002, 0x00000006, 0x00000005, 0x0000007D, 0x00000056, 0x000000F0, 0x00000028, 0x00000004, 0x00000059, 0x0000004D, 0x0000004D, 0x0000004B, 0x00000053, 0x00000009, 0x00000001, 0x0000000F, 0x00000057, 0x00000008, 0x000000D3, 0x00000038, 0x0000006F, 0x00000299, 0x000000E1, 0x00000036, 0x00000002, 0x00000076, 0x00000357, 0x0000006A, 0x000000AA, 0x00000374, 0x000001A4, 0x0000005D, 0x00000056, 0x00000057, 0x00000007, 0x0000007F, 0x00000008, 0x000000A8, 0x000000B0, 0x00000009, 0x00000032, 0x00000002, 0x00000006, 0x00000463, 0x00000469, 0x00000005, 0x000000C6, 0x00000002, 0x00000025, 0x00000068, 0x00000033, 0x00000032, 0x00000067, 0x00000001, 0x00000071, 0x00000001, 0x00000507, 0x00000063, 0x00000008, 0x00000006, 0x000000A3, 0x000005F5, 0x00000006, 0x00000031, 0x000003B8, 0x00000065, 0x00000200, 0x00000028, 0x00000057, 0x00000001, 0x000000A5, 0x00000009]
check_data=[0x00000000, 0x00000001, 0x00000002, 0x00000003, 0x00000012, 0x00000013, 0x00000014, 0x00000023, 0x00000024, 0x00000004, 0x00000005, 0x00000006, 0x00000007, 0x00000008, 0x00000015, 0x00000017, 0x00000027, 0x00000037, 0x00000010, 0x00000020, 0x00000030, 0x00000031, 0x00000040, 0x00000050, 0x00000051, 0x00000052, 0x00000060, 0x00000011, 0x00000021, 0x00000022, 0x00000032, 0x00000033, 0x00000034, 0x00000035, 0x00000041, 0x00000042, 0x00000016, 0x00000025, 0x00000026, 0x00000036, 0x00000043, 0x00000044, 0x00000045, 0x00000046, 0x00000054, 0x00000018, 0x00000028, 0x00000038, 0x00000048, 0x00000058, 0x00000067, 0x00000068, 0x00000078, 0x00000088, 0x00000047, 0x00000055, 0x00000056, 0x00000057, 0x00000065, 0x00000066, 0x00000076, 0x00000077, 0x00000087, 0x00000053, 0x00000062, 0x00000063, 0x00000064, 0x00000072, 0x00000074, 0x00000075, 0x00000085, 0x00000086, 0x00000061, 0x00000070, 0x00000071, 0x00000073, 0x00000080, 0x00000081, 0x00000082, 0x00000083, 0x00000084]

init_box()
cpuid_func(0xDEADBEEF)
invd_func(0x4437)
rdmsr(0x174)

rdmsr(0x176)                                 
invd_func(0x4433)                               
vmcall_func(0x30133403)                         
vmcall_func(0x3401CC01)
vmcall_func(0x36327A09)
vmcall_func(0x3300CC00)
vmcall_func(0x3015CC04)
vmcall_func(0x35289D07)
vmcall_func(0x3027CC06)
vmcall_func(0x3412CC03)
vmcall_func(0x3026CD06)
vmcall_func(0x34081F01)
vmcall_func(0x3311C302)
vmcall_func(0x3625CC05)
vmcall_func(0x3930CC07)
vmcall_func(0x37249405)
vmcall_func(0x34027200)
vmcall_func(0x39236B04)
vmcall_func(0x34317308)
vmcall_func(0x3704CC02)

invd_func(0x4434)
vmcall_func(0x38531F11)
vmcall_func(0x3435CC09)
vmcall_func(0x3842CC0A)
vmcall_func(0x3538CB0B)
vmcall_func(0x3750CC0D)
vmcall_func(0x3641710D)
vmcall_func(0x3855CC0F)
vmcall_func(0x3757CC10)
vmcall_func(0x3740000C)
vmcall_func(0x3147010F)
vmcall_func(0x3146CC0B)
vmcall_func(0x3743020E)
vmcall_func(0x36360F0A)
vmcall_func(0x3152CC0E)
vmcall_func(0x34549C12)
vmcall_func(0x34511110)
vmcall_func(0x3448CC0C)
vmcall_func(0x3633CC08)

invd_func(0x4437)
vmcall_func(0x3080CC17)
vmcall_func(0x37742C16)
vmcall_func(0x3271CC14)
vmcall_func(0x3983CC19)
vmcall_func(0x3482BB17)
vmcall_func(0x3567BC15)
vmcall_func(0x3188041A)
vmcall_func(0x3965CC12)
vmcall_func(0x32869C19)
vmcall_func(0x3785CC1A)
vmcall_func(0x3281CC18)
vmcall_func(0x3262DC14)
vmcall_func(0x3573CC15)
vmcall_func(0x37566613)
vmcall_func(0x3161CC11)
vmcall_func(0x3266CC13)
vmcall_func(0x39844818)
vmcall_func(0x3777CC16)
vmcall_func(0xFFEEDEAD)

print s.check()
while(s.check()==sat):
    m = s.model()
    flag2 = ""
    for i in m_input:
        flag2 += chr(m[i].as_long())
    print(flag2)
    exp = []
    for val in m_input:
        exp.append(val!=m[val])
    s.add(Or(exp))
gate_one()

1、最后在恢复代码的时候确实是很累的活，将伪C代码转换为python脚本，中间还是有一些部分需要去理解的，自己动手恢复一遍会收获很多。

2、由于写的时候，时间跨度比较大，函数名和截图不一定能对上号，双手奉上idb，作为参考。

3、相关的idb已上传至网盘

相关附件

https://pan.baidu.com/s/1FYjUhx7H1Gjx0y7rbyqocQ 密码:182w

总结

这篇文章经历的时间有点长了，不过总算是结尾了，也算是善始善终。在写作期间，先后也查看了许多别人的解法，但是总归没有自己动手。如此详实的记载一遍，一方面切实能自己动手完整的解题并留下宝贵的过程，另一面也可以分享出来给大家作为参考。文中必定还有许多内容值得推敲，如有问题，还请大家指出。

最后

v爷爷的 出题思路

夜影师傅的 解题思路

看到没有！这就是大佬！ORZ～