z3学习

发表于 | 阅读次数:

基本语法

安装好后进入z3目录下，source ~/z3/bin/activate

照着官网教程学习下

1
2
3
4
5
from z3 import *
p = Bool('p')
q = Bool('q')
r = Bool('r')
solve(Implies(p,q),r==Not(q),And(Not(p),r))

结果[q = False, p = False, r = True]

这里Implies是离散数学中的蕴含式，只有(1,0)->0

1
2
3
4
5
6
from z3 import *
x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3,x**2 + x**2 + y**2 + 2 >= 5))

simplify函数简化表达式（我猜可能类似于编译优化中的策略？）

1
2
3
3 + 3*x + y
Not(y <= -2)
And(x >= 2, 2*x**2 + y**2 >= 3)

多项式与布尔代数的结合

1
2
3
4
from z3 import *
p = Bool('p')
x = Real('x')
solve(Or(x < 5,x > 10),Or(p, x**2 == 2),Not(p))

结果[x = -1.4142135623?, p = False]

1
2
3
4
5
6
from z3 import *

x = Real('x')
s = Solver()
s.add(2**x==3)
print s.check() # unknown

这样是错误的，因为这不是线性约束条件

显示z3内部表示形式

1
2
3
4
5
from z3 import *
x,y = Ints('x y')
print (Sqrt(2) + Sqrt(3))
print simplify(Sqrt(2)+Sqrt(3))
print simplify(Sqrt(2)+Sqrt(3)).sexpr()

输出结果

1
2
3
2**(1/2) + 3**(1/2)
3.1462643699?
(root-obj (+ (^ x 4) (* (- 10) (^ x 2)) 1) 4)

遍历模型

遍历约束条件

1
2
3
4
5
6
7
8
9
from z3 import *
x = Int('x')
y = Int('y')
s = Solver()
s.add(x>1,y>1,Or(x+y>3,x-y<2))

print "assertions:"
for c in s.assertions():
	print c

可用于debug，输出如下

1
2
3
4
assertions:
x > 1
y > 1
Or(x + y > 3, x - y < 2)

解决方案是一组断言约束的模型(model)

模型是使每个断言约束成立的解释

此方法显示了如何遍历所有模型

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
from z3 import *
x = Real('x')
y = Real('y')
z = Real('z')

s = Solver()
s.add(x>1,y>1,x+y>3,z-x<10)
print s.check()

m = s.model()
print "x = %s" % m[x]
#The  expression  m[x]  returns  the  interpretation  of x in the model m

print "trasversing model"
for d in m.decls():
	print "%s = %s" % (d.name(),m[d])

输出结果：

1
2
3
4
5
6
sat
x = 3/2
trasversing model
z = 0
y = 2
x = 3/2

函数

关于函数，z3中的函数没有副作用并且是完全的(total)

1
2
3
4
5
6
7
8
9
10
11
12
13
from z3 import *

x = Int('x')
y = Int('y')

f = Function('f',IntSort(),IntSort())
s = Solver()
s.add( f( f(x) )==x, f(x)==y, x!=y)

print s.check()
m = s.model()
print "f(f(x)) = " , m.evaluate(f(f(x)))
print "f(x) = " , m.evaluate(f(x))

其中f是一个未解释的函数（之前已经提到过解释），接收一个类型（又称排序）为整数的参数并产生一个整数值

The solution(interpretation) for f should be read as f(0) is 1,f(1) is 0,and f(a) is 1 for all a different from 0 and 1.

验证摩根定律

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
from z3 import *

p,q = Bools('p q')
demorgan = And(p,q) == Not(Or(Not(p),Not(q)))
print demorgan

def prove(f):
	s = Solver()
	s.add(Not(f))
	if s.check()==unsat: #unsatisfied
		print "proved"
	else:
		print "failed to prove"

print "Proving demorgan"
prove(demorgan)

输出结果

1
2
3
And(p, q) == Not(Or(Not(p), Not(q)))
Proving demorgan
proved

以后大概很少尝试证明一些数学内容了，突然想起一句关于黎曼猜想的评论

无论对黎曼猜想的证明是否成立，仍然对Atiyah爵士一生挚爱数学致以敬意

列表推导

python支持列表推导，演示创建列表的简明方法

1
2
3
4
5
6
7
8
9
10
11
12
13
from z3 import *

print [x+1 for x in range(5)]

X = [Int('x%s'%i) for i in range(5)]
Y = [Int('y%s'%i) for i in range(5)]
print X

X_plus_Y = [ X[i]+Y[i] for i in range(5)]
print X_plus_Y

X_gt_Y = [X[i]>Y[i] for i in range(5)]
print And(X_gt_Y)

输出结果

1
2
3
4
[1, 2, 3, 4, 5]
[x0, x1, x2, x3, x4]
[x0 + y0, x1 + y1, x2 + y2, x3 + y3, x4 + y4]
And(x0 > y0, x1 > y1, x2 > y2, x3 > y3, x4 > y4)

创建3*3矩阵，两层循环

1
2
3
4
5
6
from z3 import *

x = [[ Int("x_%s_%s" % (i+1,j+1)) for j in range(3)]
	for i in range(3)]

pp(x)

其中pp()类似print，但它使用Z3Py格式化程序来表示列表和元组

输出结果

1
2
3
[[x_1_1, x_1_2, x_1_3],
 [x_2_1, x_2_2, x_2_3],
 [x_3_1, x_3_2, x_3_3]]

Z3Py还提供了创建Boolean，Integer和Real变量向量的函数，同样使用列表推导来实现

1
2
3
4
5
6
7
8
9
10
11
from z3 import *

X = IntVector('x',5)
Y = RealVector('y',5)
P = BoolVector('p',5)
print X
print Y
print P

print [y**2 for y in Y]
print Sum([y**2 for y in Y])

输出结果

1
2
3
4
5
[x__0, x__1, x__2, x__3, x__4]
[y__0, y__1, y__2, y__3, y__4]
[p__0, p__1, p__2, p__3, p__4]
[y__0**2, y__1**2, y__2**2, y__3**2, y__4**2]
y__0**2 + y__1**2 + y__2**2 + y__3**2 + y__4**2

BitVec

CTF中用的比较多的应该就是这种BitVec

1
2
3
4
5
6
7
8
9
from z3 import *

a = BitVecVal(-1,16)
b = BitVecVal(65535,16)
print simplify(a==b) # True

a = BitVecVal(-1,32)
b = BitVecVal(65535,32)
print simplify(a==b) # False

ULT是无符号数的比较之一，其余见文档

1
2
3
4
5
6
from z3 import *

x,y = BitVecs('x y',32)
solve(x+y==2,x>0,y>0)
solve(x&y == ~y)
solve(ULT(x,0)) # ULT: unsigned less than

输出结果

1
2
3
[y = 1, x = 1]
[y = 4294967295, x = 0]
no solution

逻辑移位>>最左都补0，算术移位最左补符号位，这里都是算术移位

1
2
3
4
5
6
from z3 import *

x,y = BitVecs('x y',32)
solve(x>>2==3)
solve(x<<2==3)
solve(x<<2==24)

输出结果

1
2
3
[x = 12]
no solution
[x = 6]

CTF&实例

1、解数独

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
#coding:utf-8
from z3 import *

X = [ [ Int("x_%s_%s" %(i+1,j+1)) for j in range(9)]
	for i in range(9)]

#each cell contains a value in {1...9}
cells_c = [ And(1<=X[i][j],X[i][j]<=9)
	for i in range(9) for j in range(9)]

#each row
rows_c = [Distinct(X[i]) for i in range(9)]

#each column
cols_c = [Distinct(X[i][j]) for i in range(9)
	for j in range(9)]

#each 3*3 square
sq_c =[ 
	Distinct(
	    [ X[3*i0 + i][3*j0 + j]
            for i in range(3) for j in range(3) ]
            )
    	for i0 in range(3) for j0 in range(3) 
      ]

sudoku_c = cells_c + rows_c + cols_c + sq_c

# sudoku instance, we use '0' for empty cells
instance = ((0,0,0,0,9,4,0,3,0),
            (0,0,0,5,1,0,0,0,7),
            (0,8,9,0,0,0,0,4,0),
            (0,0,0,0,0,0,2,0,8),
            (0,6,0,2,0,1,0,5,0),
            (1,0,2,0,0,0,0,0,0),
            (0,7,0,0,0,0,5,2,0),
            (9,0,0,0,6,5,0,0,0),
            (0,4,0,9,7,0,0,0,0))

#这里的If没怎么看懂，应该是必须满足instance中不等于0的数必须等于X中对应的，And手输?.....
instance_c = [ If(instance[i][j] == 0,
                  True,
                  X[i][j] == instance[i][j])
               for i in range(9) for j in range(9) ]

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
    m = s.model()
    r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
          for i in range(9) ]
    print_matrix(r)
else:
	print "failed to solve"

输出结果

1
2
3
4
5
6
7
8
9
[[5, 7, 2, 6, 9, 4, 1, 3, 8],
 [6, 4, 3, 5, 1, 8, 9, 2, 7],
 [1, 8, 9, 7, 3, 2, 5, 4, 6],
 [4, 7, 9, 3, 5, 6, 2, 1, 8],
 [8, 6, 3, 2, 7, 1, 4, 5, 9],
 [1, 5, 2, 8, 9, 4, 3, 6, 7],
 [6, 7, 3, 1, 8, 4, 5, 2, 9],
 [9, 8, 2, 3, 6, 5, 4, 7, 1],
 [1, 4, 5, 9, 7, 2, 6, 3, 8]]

2、CTF-1

HITB CTF 2016 soup meat tead

题目只给了源代码，稍作改动，如下

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
// Soup Meat Tea (SMT) (TM)
//
// We welcome you to our delicious kitchen featuring many dishes from all
// around the world. With so many choices we really don't know the perfect
// combination. Fortunately our previous chef left the best set of dishes for
// a table of 8 people. Can you reconstruct the set of dishes?
//
// The service provided by our last chef can be found at.. find the ip/port
// as if it's a stego001 challenge :-)
//
// Compile with:    gcc -std=c99 soup_meat_tea.c -o soup_meat_tea
// Test with:       echo -n $'... payload ...'|./soup_meat_tea

#include <stdio.h>
#include <stdint.h>
#include <stdlib.h>
#include <unistd.h>

uint32_t state = 42;

typedef enum {
    D_SOUP_CHICKEN,
    D_SOUP_MEAT,
    D_SOUP_NAZI,
    D_CHICKEN_RAW,
    D_CHICKEN_BLACK,
    D_MEAT_BLACKANGUS,
    D_MEAT_WAGYU,
    D_MEAT_HORSE,
    D_TIRAMISU,
    D_ICE_BANANA,
    D_ICE_STRAWBERRY,
    D_OVERFLOW,
} dish_t;

const char *dishes[] = {
    "soup-chicken", "soup-meat", "soup-nazi", "chicken-raw", "chicken-black",
    "meat-blackangus", "meat-wagyu", "meat-horse", "tiramisu", "ice-banana",
    "ice-strawberry",
};

void dish(uint8_t d)
{
    state = ((state + d) * 3294782) ^ 3159238819;
}

int main()
{
    uint8_t input[32];
    read(0, input, 32);

    for (uint32_t idx = 0; idx < 32; idx++) {
        dish(input[idx]);
    }

    printf("That's some delicious.. ");
    for (uint32_t idx = 0; idx < 32; idx++) {
        if(input[idx] < D_OVERFLOW) {
            printf("%s ", dishes[input[idx]]);
        }
        else {
            printf("%s ", "<YUEATTHIS>");
        }
    }

    if(state == 0xde11c105) {
        system("/bin/cat flag.txt");
    }
    return 0;
}

里面有很多废话，就是输入32个unsigned char，经过一堆运算后让state==0xde11c105

先给出z3的exp

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
from z3 import *
state = 42

def dish(d):
	global state
	state = ((state + d) * 3294782) ^ 3159238819

input = [BitVec('input_%d'%i,32) for i in range(32)]

for idx in range(32):
	dish(input[idx])


s = Solver()

for i in range(32):
	s.add(input[i]>=0,input[i]<=0xff)

s.add(state==0xde11c105)

if s.check()==sat:
	m = s.model()
	print m
	print repr("".join([chr(m[input[i]].as_long()) for i in range(32)]))

有一些疑问和要注意的

  1. dish函数里的global，捕获外界全局变量

  2. 因为代码中是unsigned char，我们为求简便，用BitVec表示，接着把每一个BitVec32的范围都限定在[0,255]，显然这里只用BitVec8可能是不好用的…python的类型我不熟悉，感觉挺迷的

    这里如何体现正负啊？？？算了就这么用吧

  3. C代码里由于没有体现类型…….所以直接就转成python函数了，如果有了强转，或者类型不能自动提升该如何是好？？

好吧我决定多做几个题看看wp再说

最后的结果是这样的

1

就是输入给远程程序的数据

题目中是unsigned char，根据上次南大校赛的一个错题，发现gdb调试时会出现无法解决的错误，程序读入char，pwntools一旦发出超过\x7f就会提升类型，不过这好像不是同一个问题

于是…试试echo -e | ./xxx

输出结果

2

3、CTF-3

3

z3脚本

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
from z3 import *
inp = [BitVec('a%d' %i, 56) for i in range(3)]
sol_1 = inp[0] - inp[1] + inp[2]
sol_2 = inp[1] +3 *(inp[2]+inp[0])
sol_3 = inp[2]*inp[1]

s = Solver()
s.add(sol_1==1550207830)
s.add(sol_2==12465522610)
s.add(sol_3==3651346623716053780)
print s.check()
m = s.model()
r = []
for i in inp:
    print m[i]

输出结果：

4