您好,登錄后才能下訂單哦!
如何分析Z3Py在CTF逆向中的運用,針對這個問題,這篇文章詳細介紹了相對應的分析和解答,希望可以幫助更多想解決這個問題的小伙伴找到更簡單易行的方法。
Z3是Microsoft Research開發(fā)的高性能定理證明器。Z3擁有者非常廣泛的應用場景:軟件/硬件驗證和測試,約束求解,混合系統(tǒng)分析,安全性研究,生物學研究(計算機分析)以及幾何問題。Z3Py是使用Python腳本來解決一些實際問題。
現(xiàn)在的CTF逆向中,求解方程式或者求解約束條件是非常常見的一種考察方式,而ctf比賽都是限時的,當我們已經(jīng)逆向出來flag的約束條件時,可能還需要花一定的時間去求解逆過程。而Z3求解器就給我們提供了一個非常便利求解方式,我們只需要定義未知量(x,y等),然后為這些未知量添加約束方式即可求解。Z3求解器能夠求解任意多項式,但是要注意的是,當方程的方式為2**x這種次方運算的時候,方程式已經(jīng)不是多項式的范疇了,Z3便無法求解。
現(xiàn)在我們利用官方文檔中的一個例子來粗略的看一下Z3Py的使用。
x = Int('x') y = Int('y') solve(x > 2, y < 10, x + 2*y == 7)
代碼非常簡單,首先利用Int()定義兩個int型未知數(shù)x和y,然后利用三個約束條件進行相應的求解:
x > 2
y < 10
x + 2*y == 7
由上述的代碼看得出來Z3Py的使用方式比較簡單,
定義未知量
添加約束條件
然后求解
首先我們利用IDA去打開該文件,定位到關鍵點,發(fā)現(xiàn)關鍵函數(shù)如下:
signed __int64 sub_400766() { if ( strlen((const char *)&stru_6020A0) != 32 ) return 0LL; v3 = stru_6020A0.y1; v4 = stru_6020A0.y2; v5 = stru_6020A0.y3; v6 = stru_6020A0.y4; if ( stru_6020A0.x2 * (signed __int64)stru_6020A0.x1 - stru_6020A0.x4 * (signed __int64)stru_6020A0.x3 != 0x24CDF2E7C953DA56LL ) goto LABEL_15; if ( 3LL * stru_6020A0.x3 + 4LL * stru_6020A0.x4 - stru_6020A0.x2 - 2LL * stru_6020A0.x1 != 0x17B85F06 ) goto LABEL_15; if ( 3 * stru_6020A0.x1 * (signed __int64)stru_6020A0.x4 - stru_6020A0.x3 * (signed __int64)stru_6020A0.x2 != 0x2E6E497E6415CF3ELL ) goto LABEL_15; if ( 27LL * stru_6020A0.x2 + stru_6020A0.x1 - 11LL * stru_6020A0.x4 - stru_6020A0.x3 != 0x95AE13337LL ) goto LABEL_15; srand(stru_6020A0.x3 ^ stru_6020A0.x2 ^ stru_6020A0.x1 ^ stru_6020A0.x4); v1 = rand() % 50; v2 = rand() % 50; v7 = rand() % 50; v8 = rand() % 50; v9 = rand() % 50; v10 = rand() % 50; v11 = rand() % 50; v12 = rand() % 50; if ( v6 * v2 + v3 * v1 - v4 - v5 != 0xE638C96D3LL || v6 + v3 + v5 * v8 - v4 * v7 != 0xB59F2D0CBLL || v3 * v9 + v4 * v10 - v5 - v6 != 0xDCFE88C6DLL || v5 * v12 + v3 - v4 - v6 * v11 != 0xC076D98BBLL ) { LABEL_15: result = 0LL; } else { result = 1LL; } return result; }
可以看得出來這個題目的目的就是找出滿足方程的flag。我們可以很方便的把方程式列出來,但是求解對于一些數(shù)學不是很好的人來說簡直就是噩夢,這時候Z3求解器就可以很方便的給我們幫助。我們按照題目的意思一步一步利用Z3求解器來求解:
from z3 import * x1 = Int('x1') x2 = Int('x2') x3 = Int('x3') x4 = Int('x4') s = Solver() s.add( x2*x1-x4*x3 == 0x24CDF2E7C953DA56) s.add( 3*x3+4*x4-x2-2*x1 == 0x17B85F06) s.add( 3*x1*x4-x3*x2 == 0x2E6E497E6415CF3E) s.add( 27*x2+x1-11*x4 - x3 == 0x95AE13337) print s.check() m = s.model() print "traversing model..." for d in m.decls(): print "%s = %s" % (d.name(), m[d])
Solver()命令創(chuàng)建一個通用求解器。我們可以通過add函數(shù)添加約束條件。我們稱之為聲明約束條件。check()函數(shù)解決聲明的約束條件,sat結果表示找到某個合適的解,unsat結果表示沒有解。這時候我們稱約束系統(tǒng)無解。最后,求解器可能無法解決約束系統(tǒng)并返回未知作為結果。
對于上面的題目我們首先定義x1,x2,x3,x4四個int變量,然后添加逆向中的約束條件,最后進行求解。Z3會在找到合適解的時候返回sat。我們認為Z3能夠滿足這些約束條件并得到解決方案。該解決方案被看做一組解決約束條件的模型。模型能夠使求解器中的每個約束條件都成立。最后我們遍歷model中的解。
得到x1,x2,x3,x4的解后,我們將其代入逆向題中,得出v1,v2,v7,v8,v9,v9,v10,v11,v12的值,然后進行下一步的求解:
v1 = 0x16 v2 = 0x27 v7 = 0x2d v8= 0x2d v9 = 0x23 v10= 0x29 v11 = 0xd v12 = 0x24 v3 = Int('v3') v4 = Int('v4') v5 = Int('v5') v6 = Int('v6') s = Solver() s.add(v6 * v2 + v3 * v1 - v4 - v5 == 0xE638C96D3) s.add(v6 + v3 + v5 * v8 - v4 * v7 == 0xB59F2D0CB) s.add(v3 * v9 + v4 * v10 - v5 - v6 == 0xDCFE88C6D) s.add(v5 * v12 + v3 - v4 - v6 * v11 == 0xC076D98BB) print s.check() m = s.model() print "traversing model..." for d in m.decls(): print "%s = %s" % (d.name(), m[d])
這樣的話我們就花了比較少的時間得到我們想要的flag,還是比較方便的。
但是現(xiàn)實中很多的逆向題都是基于位運算的,同樣在Z3Py中可以使用Bit_Vectors進行機器運算。它們能夠實現(xiàn)無符號和有符號二進制運算。Z3為符號數(shù)運算提供了一個特殊的運算符操作版本,其中運算符<,<=,>,> =,/,%和>>對應于有符號運算。 相應的無符號運算符是ULT,ULE,UGT,UGE,UDiv,URem和LShR。我們看一下如下的代碼就能清楚許多:
# Create to bit-vectors of size 32 x, y = BitVecs('x y', 32) solve(x + y == 2, x > 0, y > 0) # Bit-wise operators # & bit-wise and # | bit-wise or # ~ bit-wise not solve(x & y == ~y) solve(x < 0) # using unsigned version of < solve(ULT(x, 0))
Z3Py同樣支持了Python中的創(chuàng)建List的方式,我們看如下代碼:
# Create list [1, ..., 5] print [ x + 1 for x in range(5) ] # Create two lists containing 5 integer variables X = [ Int('x%s' % i) for i in range(5) ] Y = [ Int('y%s' % i) for i in range(5) ] print X # Create a list containing X[i]+Y[i] X_plus_Y = [ X[i] + Y[i] for i in range(5) ] print X_plus_Y # Create a list containing X[i] > Y[i] X_gt_Y = [ X[i] > Y[i] for i in range(5) ] print X_gt_Y print And(X_gt_Y) # Create a 3x3 "matrix" (list of lists) of integer variables X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(3) ] for i in range(3) ] pp(X)
在上面的例子中,表達式“x%s”%i返回一個字符串,其中%s被替換為i的值。命令pp與print類似,但是它使用Z3Py格式化程序而不是Python的格式化程序來使用列表和元組。
我們打開文件,也是比較直觀的看到約束條件,我試著逆向了這個過程,花費了挺多的時間才得到答案,但是如果我們使用Z3Py來求解的話就會非常的快。
函數(shù)關鍵部分如下:
int __cdecl main(int argc, const char **argv, const char **envp) { unsigned int ii; // esi unsigned int v4; // kr00_4 char flag_i; // bl unsigned int jj; // eax char *v7; // edx char v8; // cl int v9; // eax char xor_result[80]; // [esp+8h] [ebp-A4h] char flag[80]; // [esp+58h] [ebp-54h] sub_DC1020("Please input your flag: "); sub_DC1050("%40s", flag); memset(xor_result, 0, 0x50u); ii = 0; v4 = strlen(flag); if ( v4 ) { do { flag_i = flag[ii]; jj = 0; do { v7 = &xor_result[jj + ii]; v8 = flag_i ^ data1[jj++]; *v7 += v8; } while ( jj < 0x20 ); ++ii; } while ( ii < v4 ); } v9 = strcmp(xor_result, (const char *)&data2); if ( v9 ) v9 = -(v9 < 0) | 1; if ( v9 ) puts("No, it isn't."); else puts("Yes, it is."); return 0; }
很簡潔明了,我們利用Z3Py來進行變量的聲明和約束的增加并進行求解
from z3 import * s = Solver() X = [BitVec(('x%s' % i),8) for i in range(0x22) ] data1 = [0x21,0x22,0x23,0x24,0x25,0x26,0x27,0x28,0x29,0x2A,0x2B,0x2C,0x2D,0x2E,0x2F,0x3A, 0x3B,0x3C,0x3D,0x3E,0x3F,0x40,0x5B,0x5C,0x5D,0x5E,0x5F,0x60,0x7B,0x7C,0x7D,0x7E] data2 = [0x72,0xE9,0x4D,0xAC,0xC1,0xD0,0x24,0x6B,0xB2,0xF5,0xFD,0x45,0x49,0x94,0xDC,0x10, 0x10,0x6B,0xA3,0xFB,0x5C,0x13,0x17,0xE4,0x67,0xFE,0x72,0xA1,0xC7,0x04,0x2B,0xC2, 0x9D,0x3F,0xA7,0x6C,0xE7,0xD0,0x90,0x71,0x36,0xB3,0xAB,0x67,0xBF,0x60,0x30,0x3E, 0x78,0xCD,0x6D,0x35,0xC8,0x55,0xFF,0xC0,0x95,0x62,0xE6,0xBB,0x57,0x34,0x29,0x0E,3] xor_result = [0]*0x41 for m in range(0,0x22): for n in range(0,0x20): xor_result[n+m] += X[m] ^ data1[n] for o in range(0,0x41): s.add(xor_result[o] == data2[o]) print s.check() m = s.model() print "traversing model..." for i in range(0,0x22): print chr(int("%s" % (m[X[i]]))),
很簡單的幾行代碼,聲明0x22個8位BitVec的未知數(shù),獲取數(shù)據(jù),然后增加約束條件,求解,這樣就能夠幫助我們獲取flag。
雖然CTF逆向比賽中重點考察的是逆向的能力,采用求解器的方式來求解并不能鍛煉到自己的逆向邏輯,REConvolution逆向題目有一個非常清晰明了的逆過程,還是很有趣的。
關于如何分析Z3Py在CTF逆向中的運用問題的解答就分享到這里了,希望以上內容可以對大家有一定的幫助,如果你還有很多疑惑沒有解開,可以關注億速云行業(yè)資訊頻道了解更多相關知識。
免責聲明:本站發(fā)布的內容(圖片、視頻和文字)以原創(chuàng)、轉載和分享為主,文章觀點不代表本網(wǎng)站立場,如果涉及侵權請聯(lián)系站長郵箱:is@yisu.com進行舉報,并提供相關證據(jù),一經(jīng)查實,將立刻刪除涉嫌侵權內容。