Z3

CRYPTO · 知识域。SMT 约束求解在密码题中的应用。标签:Z3解密方程组。

触发特征

  • 题面是"方程组/约束系统":校验逻辑、异或方程、字节约束、自定义 VM 校验。
  • 逆向拿到 check 函数后"约束太繁不想手推"。

Z3解密方程组

  • 建模原则:
  • 位级(异或/移位/截断)用 BitVec;算术未知规模用 Int;实数精度用 Real。
  • 逐字符建模 flag[i] 并加可打印约束(0x20-0x7e)或前缀约束(flag{)。
  • 求解模板:
from z3 import *
s = Solver()
f = [BitVec(f'f{i}', 8) for i in range(N)]
for c in f: s.add(c >= 0x20, c <= 0x7e)
s.add(校验表达式 == 目标)
s.check(); m = s.model()
  • 密文方程组:轮函数不可逆(如取模压缩)时正向建模全约束,Z3 反解输入。
  • 多解处理:s.check() == sat 后加 s.add(Or([x != m[x] for x in f])) 枚举;解唯一性验证。

典型场景

  • 流密码约束:LFSR/非线性生成器的状态-输出约束(→ LFSR)。
  • 布尔门网络 SAT:产品 key/电路校验(BSIDSSF 2026)。
  • 元胞自动机逆推:Rule 86 PRNG 反转(2018)。
  • VM/解释器校验:printf 格式串 VM 反编译到 Z3(SECCON 2017);单行 Python 布尔电路(BearCatCTF 2026)。
  • seccomp/BPF 过滤分析:位向量建模过滤规则找放行 syscall(Pwn 联动)。
  • 哈希小规模逆像:自定义/弱哈希(截断 SHA)有限位宽反解。
  • 拼图/调度类:数独化、N-Queens 化的杂项题。

性能与坑

  • 解不出来:改位宽(Int↔BitVec)、拆中间变量(命名每步)、加对称破缺约束、限制解空间。
  • simplify() 先化简再解;超时用增量求解(push/pop)。
  • Z3 解出后**务必回代验证**——模型可能绕过未声明的隐式约束(类型宽度溢出等)。

工具速查

pip install z3-solver
# 大规模布尔系统可换 boolector/Cryptominisat(SECCON 2017 同类题 boolector SMT2)

转向

  • 校验逻辑在二进制里 → Reverse;线性系统规模小直接高斯 → 数理

评论