z3学习档案

Reference：

看雪-z3巧解逆向

知乎:Z3一把梭

z3 solver学习

使用z3约束求解器解决CTF中的题目

Playing with Z3,hacking the serial check

Z3 - 第一次簡單小練習

安装

pip install z3-solver

使用方法

>>> from z3 import *
>>> x = Int('x')
>>> y = Int('y')
>>> a = Real('a')
>>> b = Real('b')
>>> c = Real('c')
>>> d = Real('d')
>>> s = Solver()
>>> s.add(a + b == 12)
>>> s.add(c - d == 9)
>>> s.add(a + c == 22)
>>> s.add(b + d == 12)
>>> 
>>> print(s.check())
sat
>>> print(s.model())
[b = 11/2, a = 13/2, d = 13/2, c = 31/2]
>>> p = Solver()
>>> p.add(x + y == 1567856551)
>>> p.add(x - y == 6535435)
>>> p.check()
sat
>>> p.model()
[x = 787195993, y = 780660558]

可以使用'Int','Real','BitVec'等声明一个整数或实数变量，也可以申明一个变量数组，如

knownarr = [IntVal(i) for i in encrypted]
message = [Int('flag%d' % i) for i in range(len(encrypted)-1)]
first = IntVector(‘a’, 4)

后面都可以通过arrayname[id]进行访问

Solver()创建求解器

.add为变量之间增加约束条件

.check()检查约束条件是否ok

.model()列出求解结果

实例

ISCC2018 Reverse150

验证函数为两个方程组，解第一个方程组获得种子，而后将字符串按照int进行解析，得到第二个方程组

按照原逻辑声明变量，添加方程组约束条件即可

Attention:

> Int类型函数无法顺利表示过大的数，使用BitVec('x',64)可以声明在64bit之内的变量。

> 使用ctypes库，可以调用c语言的函数等

#!/usr/bin/env python
# -*-coding=utf-8-*-
from z3 import *
import ctypes
from pwn import *

# context.log_level = 'debug'
s = Int('s')
s1 = Int('s1')
s2 = Int('s2')
s3 = Int('s3')

ans = Solver()
ans.add(s1 * s - s3 * s2 == 2652042832920173142)
ans.add(3 * s2 + 4 * s3 - s1 - 2 * s == 397958918) 
ans.add(3 * s *s3 - s2 * s1 ==  3345692380376715070)
ans.add(27 * s1 + s - 11 * s3 - s2 ==  40179413815)

if ans.check():
    result = ans.model()
    print result

s3 = 862734414
s2 = 829124174
s1 = 1801073242
s = 1869639009

seed = s ^ s1 ^ s2 ^ s3
dll = ctypes.CDLL("/lib/x86_64-linux-gnu/libc.so.6")
dll.srand(seed)
v1 = dll.rand() % 50;
v2 = dll.rand() % 50;
v7 = dll.rand() % 50;
v8 = dll.rand() % 50;
v9 = dll.rand() % 50;
v10 = dll.rand() % 50;
v11 = dll.rand() % 50;
v12 = dll.rand() % 50;

v3 = BitVec('v3',64)
v4 = BitVec('v4',64)
v5 = BitVec('v5',64)
v6 = BitVec('v6',64)

res = Solver()
res.add(v6 * v2 + v3 * v1 - v4 - v5 == 61799700179)
res.add(v6 + v3 + v5 * v8 - v4 * v7 == 48753725643)
res.add(v3 * v9 + v4 * v10 - v5 - v6 == 59322698861)
res.add(v5 * v12 + v3 - v4 - v6 * v11 == 51664230587)
# what's this fucking do?
while res.check() == sat:
    print res.model()
    print '
---------------------'
    res.add(Or(res.model()[v3] != v3, res.model()[v4] != v4, res.model()[v5] != v5, res.model()[v6] != v6))

v6 = 1195788129
v4 = 828593230
v3 = 811816014
v5 = 1867395930
io = process("./Reverse")
payload = p32(s) + p32(s1) + p32(s2) + p32(s3)
payload += p32(v3) + p32(v4) + p32(v5) + p32(v6)

io.recvuntil('=
=======================================
')
io.sendline(payload)
io.interactive()
io.close()

高阶用法