HCTF逆向題目詳析
前言
很有水平的一場比賽，RE的幾道題目質量都非常高。
由於自己的原因，只是看了題，沒做，感覺就算認真做，也做不出來幾題，畢竟太菜。哈哈！
下面就先從最簡單的開始寫！
seven
簡單的簽到題，只不過是放在了windows驅動裡，從沒接觸過，稍微帶來了一點麻煩，演算法是很經典的吃豆子游戲，剛好看加解密時看到了，在鍵盤掃描碼卡了很久。
關於驅動開發的一些API可以在 ofollow,noindex" target="_blank">MDSN 上找到相關說明
如DriverEntry函式就是一個驅動程式的入口函式，過多的我就不班門弄斧了。
總之這個題就是有不認識的API，就直接在MDSN上找函式說明即可。
關於解題，還是搜尋字串，找到The input is the flag字樣，交叉引用到sub_1400012F0函式，如果看過加解密的同學，應該能一眼看出這是吃豆子游戲（這可不是打廣告），細看還真是！
就是如下這個矩陣
Line"/>
從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指令
Puts the logical processor in VMX operation with no current VMCS, blocks INIT signals, disables A20M, and clears any address-range monitoring established by the MONITOR instruction.10
參考連結這個指令是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_CPUID10 #defineEXIT_REASON_INVD13 #defineEXIT_REASON_VMCALL18 #defineEXIT_REASON_CR_ACCESS28 #defineEXIT_REASON_MSR_READ31 #defineEXIT_REASON_MSR_WRITE32
以上圖片來自上面的部落格
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～