Z3Py for CTF

发布于 2019-10-11  29 次阅读


TL; DR

Z3 is a high performace theorem prover developed by Microsoft. And Z3Py is Z3 API in Python.

In some reverse or crypto questions in CTF, Z3 is a powerful tool to solve your euqations and return the answer to you.


Install

% sudo pip install z3 z3-solver

If it doesn't work, maybe you can try to install z3 from the source code:

https://pypi.org/project/z3-solver/#files

% wget https://files.pythonhosted.org/packages/7c/65/2656e6157f921cb3b28999d2441997d069f6e94b9e077a614064702f09df/z3-solver-4.8.6.0.tar.gz
% tar -zxvf z3-solver-4.8.6.0.tar.gz
% cd z3-solver-4.8.6.0
% python setup.py build
% python setup.py install

Getting started

>>> from z3 import *
>>> x = Int('x') # create an interger variable in Z3 named x
>>> y = Int('y') # create an interger variable in Z3 named y
>>> solve(x > 2, y < 10, x + 2*y == 7) # solve a system of constraints
[y = 0, x = 7]
>>> from z3 import *
>>> x1 = Int('x1')
>>> x2 = Int('x2')
>>> x3 = Int('x3')
>>> x4 = Int('x4')
>>> s = Solver() # create a general purpose solver
>>> s.add( x2*x1-x4*x3 == 0x24CDF2E7C953DA56) # constraints can be added using the method add()
>>> 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() # solve the asserted constraints
sat # the result is sat(satisifable) or unsat(unsatisfiable)
>>> m = s.model() # final solution. we say the solution is a "model" for the set of asserted constrains
>>> print m
[x2 = 1801073242,
 x4 = 862734414,
 x3 = 829124174,
 x1 = 1869639009]
>>> for d in m.decls():
...     print "%s = %s" % (d.name(), m[d])
...
x2 = 1801073242
x4 = 862734414
x3 = 829124174
x1 = 1869639009
>>> from z3 import *
>>> a = Int('a') # declare single interger variable at once
>>> b, c, d = Ints('b c d') # declare multiple interger variables at once
>>> e = Real('e') # create the real variable e
>>> f, g, h = Reals('f g h')
>>> i, j, k = BitVecs('i, j, k', 8) # declare three bit-vectors variables with 8 bits
>>> solve(i^j&k == 12, j&i>>3 == 3, k^j == 4) # it works like this
[j, = 23, k = 19, i, = 31]