遇到一个需要计算的题，逆向不出来，就想想使用正向求解，z3了解一下

什么是z3

Z3 is a theorem prover from Microsoft Research. It >is licensed under the MIT license.

If you are not familiar with Z3, you can start >here.

Pre-built binaries for releases are available from >here, and nightly builds from here.

Z3 can be built using Visual Studio, a Makefile or >using CMake. It provides bindings for several >programming languages.

See the release notes for notes on various stable >releases of Z3.

就是一个约束器，可以简单理解为解方程的东西。

z3英文文档

z3翻译文档

通俗易懂

z3有三种变量类型

Int型

这种就像是我们平常说的整型，一般简单运算都可以用这个，用运算符<， <=， >， > =， ==和 ！=来进行比较

案例

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

RealVal型

就是小数形式，使用的很多，

案例

x = Real('x')
y = Real('y')
solve(x**2 + y**2 == 3, x**3 == 2)

set_option(precision=30)
print "Solving, and displaying result with 30 decimal places"
solve(x**2 + y**2 == 3, x**3 == 2)

BitVec型

现代CPU和主流编程语言使用固定大小的位向量进行算术运算。机器算法在Z3Py中可用Bit-Vectors来表示。
它实现了无符号和有符号二补数算术的精确表示，只有这个类型才可以使用异或等位运算

案例

x = BitVec('x', 16)
y = BitVec('y', 16)
print x + 2
# Internal representation
print (x + 2).sexpr()

# -1 is equal to 65535 for 16-bit integers 
print simplify(x + y - 1)

# Creating bit-vector constants
a = BitVecVal(-1, 16)
b = BitVecVal(65535, 16)
print simplify(a == b)

a = BitVecVal(-1, 32)
b = BitVecVal(65535, 32)
# -1 is not equal to 65535 for 32-bit integers 
print simplify(a == b)

一些命令如下

命令	效果
set_option(rational_to_decimal=True)	设置结果全局十进制表示
set_option(precision=30)	设置结果小数点后位数表示
simplify	化简之后约束条件
assertions	显示全部约束条件

CTF案例

文件地址
主要IDA逻辑

from z3 import *
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, 0x03]

s = Solver()
xor_res = [0]*0x41
k = [BitVec(("k%s"%i),8) for i in range(0x22)]
for i in k:
    s.add(i>0x20,i<0x7E)
for m in range(0x22):
    for n in range(0x20):
        xor_res[m+n] += k[m]^data1[n]
for j in range(0x41):
    s.add(xor_res[j]==data2[j])
print(s.check())
aa = s.model()
for i in range(0x22):
    print(chr(int('%s'%aa[k[i]])),end='')

几秒解出，很方便

---