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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
from z3 import *
def rol1_byte(value: int, shift: int) -> int:
"""Rotate left 1 byte (8 bits) with carry-over"""
shift %= 8
return ((value << shift) | (value >> (8 - shift))) & 0xFF
def transform_data(input_data: bytes) -> bytearray:
"""
Replicates the transformation logic from the original code:
- Processes each byte with a custom bit manipulation algorithm
- Uses a rolling state (v29) that affects subsequent bytes
- Applies XOR with transformed index values
"""
n = len(input_data)
output = bytearray(n)
v29 = (input_data[1] << 8) | input_data[0]
for i in range(n):
# HIWORD/LOWORD simulation (assuming v33 is 32-bit)
hiword = (v29 >> 2) ^ (v29 >> 3) ^ (v29 >> 1)
loword = v29
v33 = (hiword << 16) | (loword & 0xFFFF)
v29 = v33 >> 1
# Bit manipulation steps
v34 = rol1_byte(v33 & 0xFF, 4) # __ROL1__(v33, 4)
v35 = (4 * (v34 & 0x33)) | ((v34 >> 2) & 0x33)
# Final XOR operation
transformed_index = i + ((2 * (v35 & 0x55)) | ((v35 >> 1) & 0x55))
output[i] = input_data[i] ^ (transformed_index & 0xFF)
return output
# 目标密文
Buf2 = bytes([
0x00, 0xA1, 0xFB, 0x53, 0x1C, 0xFA, 0xF0, 0x1B, 0x06, 0x40, 0xD4, 0x8C, 0x16, 0xF4, 0x90, 0x27,
0x42, 0xB9, 0x8B, 0x0F, 0x02, 0xD7, 0x31, 0xB7, 0x26, 0x12, 0x06, 0x7E, 0xAE, 0xDF, 0xDA, 0x68,
0xAF, 0x35, 0xCC, 0xB7, 0xB0, 0xD0, 0x9A, 0x59, 0x2B, 0x0B
])
# 创建 Z3 求解器
solver = Solver()
# 定义输入变量（每个字节是一个 8 位无符号整数）
input_bytes = [BitVec(f'byte_{i}', 8) for i in range(len(Buf2))]
# 初始化状态变量 v29 (32-bit)
#v29 = BitVecVal(0, 32)
v29 = Concat(input_bytes[1], input_bytes[0])
for i in range(len(Buf2)):
# HIWORD/LOWORD 计算
hiword = (v29 >> 2) ^ (v29 >> 3) ^ (v29 >> 1)
loword = v29
v33 = Concat(Extract(15, 0, hiword), Extract(15, 0, loword))
# 更新 v29
v29 = v33 >> 1
# ROL1(v33, 4) - 取最低字节并循环左移4位
v34_lowbyte = Extract(7, 0, v33)
v34 = RotateLeft(v34_lowbyte, 4)
# v35 = (4 * (v34 & 0x33)) | ((v34 >> 2) & 0x33)
# 修正后的计算方式：
part1 = (v34 & 0x33) << 2
part2 = (v34 >> 2) & 0x33
v35 = part1 | part2
# transformed_index = i + ((2 * (v35 & 0x55)) | ((v35 >> 1) & 0x55))
part_a = (v35 & 0x55) << 1
part_b = (v35 >> 1) & 0x55
transformed_index = i + (part_a | part_b)
# 添加约束：input_byte ^ (transformed_index的低8位) == cipher_byte
solver.add(input_bytes[i] ^ Extract(7, 0, transformed_index) == Buf2[i])
# 检查是否有解
solver.add(input_bytes[0] == ord('f'))
solver.add(input_bytes[1] == ord('l'))
solver.add(input_bytes[2] == ord('a'))
solver.add(input_bytes[3] == ord('g'))
def get_models(s, count = 1):
result = []
while len(result) < count and s.check() == sat:
m = s.model()
sol = bytes([m[input_bytes[i]].as_long() for i in range(len(Buf2))])
result.append(sol)
# Create a new constraint the blocks the current model
block = []
for d in m:
# d is a declaration
if d.arity() > 0:
raise Z3Exception("uninterpreted functions are not supported")
# create a constant from declaration
c = d()
if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
raise Z3Exception("arrays and uninterpreted sorts are not supported")
block.append(c != m[d])
s.add(Or(block))
return result
m = get_models(solver, 1000)
print(m)
|
