z3的使用

在crypto中，经常会遇到某些带有限制的方程，有一些可以用线性代数的语言翻译，但有些则不行，比如与运算或运算，没办法简单用线性代数求解，那么这时候就需要z3

一、求解带不等式的方程

声明变量

1
x = Int('x')

solve可以解决方程

1
2
3
4
5
from z3 import *

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

可以解决这样的方程问题

二、求解非多项式约束，例如位运算

假设我们有一个方程：

1
(x & 0xFF) ^ (x >> 8) == 0x37

其中 x 是一个 16 位的变量（即 0 ≤ x < 65536），我们希望找到满足条件的 x。

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

# 创建 16 位变量
x = BitVec('x', 16)  # 16-bit 变量

# 创建求解器
solver = Solver()

# 添加约束条件
solver.add((x & 0xFF) ^ (x >> 8) == 0x37)

# 检查是否有解
if solver.check() == sat:
    model = solver.model()
    print("x =", hex(model[x].as_long()))
else:
    print("无解")

用这个可以解决西电的问题

1
2
3
4
5
6
7
def calculate_level1(m, x, y):

  return (m | x) + (m | y)

def calculate_level2(m, x, y):

  return (m | x) + (m ^ y)

我们有机会对m赋值两次，求x，y