z3学习档案

Reference：

安装

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 '\n---------------------'

    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('=\n=======================================\n')

io.sendline(payload)

io.interactive()

io.close()

高阶用法

作者：辣鸡小谱尼

出处：http://www.cnblogs.com/ZHijack/

如有转载，荣幸之至！请随手标明出处；

巴特西

z3学习档案

最新文章

热门文章