z3-study
最近做了个逆向题，其中有一步卡了好久（主要是最近没做这个）。是解如下方程：
其中a,b,c,d已知。问了问GPT，说是暴力枚举。x,y,z,t都是0-255的未知数，暴力枚举的话感觉耗费的时间很长，所以就想着用z3来解决。本来想着直接for来着，测了测，一轮就超1min了，属实顶不住。
0x00
z3是一个求解器。参考文档：
http://www.manongjc.com/detail/19-duecxojsjotsdln.html
0x01
上述方程该咋写咧：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
'''
# @Time : 2022/12/16 15:34:02
# @Author: wd-2711
'''
from z3 import *
if __name__ == "__main__":
x = BitVec('x', 8)
y = BitVec('y', 8)
z = BitVec('z', 8)
t = BitVec('t', 8)
a = 60
b = 61
c = 62
d = 63
solver = Solver()
solver.add(x ^ (((x^y) << 1) ^ (27 *((x^y) >> 7))) == a)
solver.add(y ^ (((z^y) << 1) ^ (27 *((z^y) >> 7))) == b)
solver.add(z ^ (((z^t) << 1) ^ (27 *((z^t) >> 7))) == c)
solver.add(t ^ (((t^x) << 1) ^ (27 *((t^x) >> 7))) == d)
solver.check()
print(solver.model())
|