前言

Z3是Microsoft Research開(kāi)發(fā)的高性能定理證明器。Z3擁有者非常廣泛的應(yīng)用場(chǎng)景：軟件/硬件驗(yàn)證和測(cè)試，約束求解，混合系統(tǒng)分析，安全性研究，生物學(xué)研究（計(jì)算機(jī)分析）以及幾何問(wèn)題。Python學(xué)習(xí)

CTF逆向中的應(yīng)用

現(xiàn)在的CTF逆向中，求解方程式或者求解約束條件是非常常見(jiàn)的一種考察方式，而ctf比賽都是限時(shí)的，當(dāng)我們已經(jīng)逆向出來(lái)flag的約束條件時(shí)，可能還需要花一定的時(shí)間去求解逆過(guò)程。而Z3求解器就給我們提供了一個(gè)非常便利求解方式，我們只需要定義未知量（x,y等），然后為這些未知量添加約束方式即可求解。Z3求解器能夠求解任意多項(xiàng)式，但是要注意的是，當(dāng)方程的方式為2**x這種次方運(yùn)算的時(shí)候，方程式已經(jīng)不是多項(xiàng)式的范疇了，Z3便無(wú)法求解。

基本使用

現(xiàn)在我們利用官方文檔中的一個(gè)例子來(lái)粗略的看一下Z3Py的使用。

x = Int('x')

y = Int('y')

solve(x > 2, y < 10, x + 2*y == 7)

代碼非常簡(jiǎn)單，首先利用Int()定義兩個(gè)int型未知數(shù)x和y，然后利用三個(gè)約束條件進(jìn)行相應(yīng)的求解：

1. x > 2

2. y < 10

3. x + 2*y == 7

由上述的代碼看得出來(lái)Z3Py的使用方式比較簡(jiǎn)單，

1. 定義未知量

2. 添加約束條件

3. 然后求解

CTF中的示例

XXX比賽中的逆向題

首先我們利用IDA去打開(kāi)該文件，定位到關(guān)鍵點(diǎn)，發(fā)現(xiàn)關(guā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;

}

可以看得出來(lái)這個(gè)題目的目的就是找出滿足方程的flag。我們可以很方便的把方程式列出來(lái)，但是求解對(duì)于一些數(shù)學(xué)不是很好的人來(lái)說(shuō)簡(jiǎn)直就是噩夢(mèng)，這時(shí)候Z3求解器就可以很方便的給我們幫助。我們按照題目的意思一步一步利用Z3求解器來(lái)求解：

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)建一個(gè)通用求解器。我們可以通過(guò)add函數(shù)添加約束條件。我們稱之為聲明約束條件。check()函數(shù)解決聲明的約束條件，sat結(jié)果表示找到某個(gè)合適的解，unsat結(jié)果表示沒(méi)有解。這時(shí)候我們稱約束系統(tǒng)無(wú)解。最后，求解器可能無(wú)法解決約束系統(tǒng)并返回未知作為結(jié)果。

對(duì)于上面的題目我們首先定義x1,x2,x3,x4四個(gè)int變量，然后添加逆向中的約束條件，最后進(jìn)行求解。Z3會(huì)在找到合適解的時(shí)候返回sat。我們認(rèn)為Z3能夠滿足這些約束條件并得到解決方案。該解決方案被看做一組解決約束條件的模型。模型能夠使求解器中的每個(gè)約束條件都成立。最后我們遍歷model中的解。

得到x1,x2,x3,x4的解后，我們將其代入逆向題中，得出v1,v2,v7,v8,v9,v9,v10,v11,v12的值，然后進(jìn)行下一步的求解：

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])

這樣的話我們就花了比較少的時(shí)間得到我們想要的flag，還是比較方便的。

但是現(xiàn)實(shí)中很多的逆向題都是基于位運(yùn)算的，同樣在Z3Py中可以使用Bit_Vectors進(jìn)行機(jī)器運(yùn)算。它們能夠?qū)崿F(xiàn)無(wú)符號(hào)和有符號(hào)二進(jìn)制運(yùn)算。Z3為符號(hào)數(shù)運(yùn)算提供了一個(gè)特殊的運(yùn)算符操作版本，其中運(yùn)算符<，<=，>，> =，/，％和>>對(duì)應(yīng)于有符號(hào)運(yùn)算。 相應(yīng)的無(wú)符號(hào)運(yùn)算符是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)

在上面的例子中，表達(dá)式“x％s”％i返回一個(gè)字符串，其中％s被替換為i的值。命令pp與print類似，但是它使用Z3Py格式化程序而不是Python的格式化程序來(lái)使用列表和元組。

第八屆極客大挑戰(zhàn)的REConvolution

我們打開(kāi)文件，也是比較直觀的看到約束條件，我試著逆向了這個(gè)過(guò)程，花費(fèi)了挺多的時(shí)間才得到答案，但是如果我們使用Z3Py來(lái)求解的話就會(huì)非常的快。

函數(shù)關(guān)鍵部分如下：

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;

}

很簡(jiǎn)潔明了，我們利用Z3Py來(lái)進(jìn)行變量的聲明和約束的增加并進(jìn)行求解

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]]))),

很簡(jiǎn)單的幾行代碼，聲明0×22個(gè)8位BitVec的未知數(shù)，獲取數(shù)據(jù)，然后增加約束條件，求解，這樣就能夠幫助我們獲取flag。