# python

Z3Microsoft Research开发的高性能定理证明器。Z3拥有者非常广泛的应用场景：软件/硬件验证和测试，约束求解，混合系统分析，安全性研究，生物学研究（计算机分析）以及几何问题。Python学习

CTF逆向中的应用

x = Int(’x’)

y = Int(’y’)

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

1. x > 2

2. y < 10

3. x + 2*y == 7

1. 定义未知量

2. 添加约束条件

3. 然后求解

CTF中的示例

XXX比赛中的逆向题

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;

}

from z3 import *

x1 = Int(’x1’)

x2 = Int(’x2’)

x3 = Int(’x3’)

x4 = Int(’x4’)

s = Solver()

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

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

# 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中的创建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)

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_DC1050("%40s", flag);

memset(xor_result, 00x50u);

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;

}

from z3 import *

s = Solver()

X =  [BitVec((’x%s’ % i),8for 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):

print s.check()

m = s.model()

print "traversing model..."

for i in range(0,0x22):

print chr(int("%s" % (m[X[i]]))),

python

(0)
(0)

0条

关注此人  发短消息

wjunxi”关注的人------（0
wjunxi”的粉丝们------（0