一 安裝：

z3是由微軟公司開發的一個優秀的SMT求解器（也就定理證明器），它能夠檢查邏輯表達式的可滿足性。

我是在windows下pyCharm 里面自己添加包 包名為z3-slover（不是z3）

二 使用：

庫內函數：

1.創建一個解的聲明對象：

s = Solver()

2.添加條件：

s.add(判斷公式)

3.判斷是否有解：

s.check()

如果有解 則反回sate/sat?反之 返回 unsate/unsat

4.返回最后的解：

result=s.modul()print(result)

5.聲明不同類型的未知數：
?

a, s, d = Ints('a s d')#創建一個‘int’類型的對象，但其實運算時候是'ArithRef'類型，#并且無法使用按位運算 x = Real('x') #創建一個有理數類型的變量。 y = Real('y')

z3庫最牛逼的來了:上面兩個就是比正常多元未知數復雜了點，求解按位運算才是這個庫最吊的！

BitVecs(name,bv,ctx=None),創建一個有多變量的位向量，name是名字，bv表示大小 #a,b,c=s=BitVecs('a b c',32) Bitvex(name,bv,ctx=None),創建一個位向量，name是他的名字，bv表示大小 BitVecSort(bv,ctx=None),創建一個指定大小的位向量 BitVecVal(val,bv,ctx=None),創建一個位向量，有初始值，沒名字

三：例題

大概使用流程：

from z3 import * a, b, c=BitVecs('a b c',32) d, e, f=BitVecs('d e f',32) g, h, i=BitVecs('g h i',32) key=[a,b,c,d,e,f,g,h] s = Solver() s.add()check = s.check() print(check) model = s.model() print(model)

四:CTF逆向的使用

對于一些較為復雜的算法，我們很難逆向或者爆破求出他的最終結果，這時可以使用z3庫正向幫助我們解決問題。

特殊代碼

X = ?[BitVec(('x%s' % i),8) for i in range(0x22) ]? ?聲明一個列表，數據類型是向量，形式是 xi，向量的大小是8

[x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33]

.as_long()函數可以把z3庫里面特殊的類型轉換成long類型

例如： res.append(chr(m[flag[i]].as_long()))

例題：第八屆極客大挑戰REConvolution

關鍵代碼：

int __cdecl main(int argc, const char **argv, const char **envp) {unsigned int ii; // esiunsigned int v4; // kr00_4char flag_i; // blunsigned int jj; // eaxchar *v7; // edxchar v8; // clint v9; // eaxchar 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.");elseputs("Yes, it is.");return 0; }

逆向很難求解，我們試試z3正向求解。

from z3 import * s = Solver() X = [BitVec(('x%s' % i),8) for i in range(0x22) ] print (X) 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...") flag='' for i in range(0,0x22):flag+=chr(int("%s" % (m[X[i]]))) print(flag)

總結

以上是生活随笔為你收集整理的CTF Re-Python z3库的使用的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。