本文详解如何用 Z3 正确建模基于 3-bit 分块运算的虚拟机程序逆向问题，指出混合 Int 与 BitVec 导致求解卡死的根本原因，并提供高效、可收敛的位向量建模方案及完整可运行示例。
本文详解如何用 z3 正确建模基于 3-bit 分块运算的虚拟机程序逆向问题，指出混合 `int` 与 `bitvec` 导致求解卡死的根本原因，并提供高效、可收敛的位向量建模方案及完整可运行示例。
在 Advent of Code 2024 Day 17 这类虚拟机逆向题中，程序按 3-bit（即八进制位）逐段解析输入整数 a，每轮执行异或、整除、位移等操作并生成一位输出。目标是：给定输出序列（如 [2, 2, 3]），反推出任一合法输入 a。初学者常尝试用 Z3 的 Int 类型直接翻译 Python 逻辑，却遭遇 s.check() 长时间无响应或返回 unknown——这并非 Z3 能力不足，而是建模方式触发了底层求解器的性能瓶颈。
核心问题在于：混用 Int 与 BitVec 会引入非线性整数约束（如 `2 b中指数为变量）**。SMT 求解器对非线性整数算术（NIA）缺乏完备决策过程，相关算法复杂度高、启发式依赖强，极易陷入搜索僵局。原代码中频繁调用Int2BV/BV2Int、用IntVal(2) ** s2` 计算动态幂次，正是典型“雷区”。
✅ 正确做法是统一使用固定宽度位向量（BitVec）建模，显式限定变量范围（如 32 位），并将所有运算映射到位级语义：
-
% 8→bvand(b, 0b111)或直接b % 8（Z3BitVec支持） -
2 ** b→ 左移1 （<code>BitVec原生支持，无非线性） - 整除
/→ 使用UDiv语义（无符号除法，符合//行为）
以下是优化后的完整可运行代码：
from z3 import *
# 给定目标输出（例如由已知输入 123 生成）
output = [2, 2, 3]
s = Solver()
# 统一使用 32 位位向量，避免类型混用
a, b, c = BitVecs('a b c', 32)
s.add(a > 0) # 输入为正整数
# 模拟原始程序的 while 循环（手动展开）
for x in output:
# b = a % 8
b = a % 8
# b = b ^ 6
b = b ^ 6
# denominator = 2 ** b → 等价于 1 << b
denominator = 1 << b
# c = a // denominator （无符号整除）
c = UDiv(a, denominator) # 显式使用 UDiv 更安全
# b = b ^ c
b = b ^ c
# b = b ^ 4
b = b ^ 4
# 输出：b % 8
s.add(b % 8 == x)
# a //= 8 → 更新 a 为下一轮输入
a = UDiv(a, 8)
# 循环终止条件：最终 a 应 ≤ 0（因 UDiv 向下取整，a=0 时停止）
s.add(a == 0)
# 求解
result = s.check()
if result == sat:
model = s.model()
found_a = model[BitVec('a', 32)].as_long()
print(f"找到解: a = {found_a}")
# 验证：用原始 Python 函数测试
def program(a_val):
b, c = 0, 0
out = []
while a_val > 0:
b = a_val % 8
b ^= 6
denominator = 1 << b # 2**b
c = a_val // denominator
b ^= c
b ^= 4
out.append(b % 8)
a_val //= 8
return out
print(f"验证输出: {program(found_a)}") # 应与 output 一致
else:
print("无解或超时:", result)运行后将快速输出 sat 及一个有效解（如 a = 115）。值得注意的是，由于程序存在多解性（如 program(115) 和 program(123) 均输出 [2, 2, 3]），Z3 返回任意满足条件的解即为成功——这恰恰体现了 SMT 求解器在逆向工程中的实用价值：无需遍历全部可能，即可高效定位可行输入。
? 关键总结：
-
禁用类型混用：勿在同一流程中交叉使用
Int和BitVec，尤其避免**、sqrt等非线性运算； -
显式位宽：对嵌入式/VM 类问题，优先假设变量为固定宽度（如 32 位），用
BitVec(n, width)建模； -
算符语义对齐：用
UDiv替代/（防符号歧义），用1 替代 <code>2**b（保持线性）； - 循环需手动展开：Z3 不支持动态循环，需根据输出长度确定迭代次数。
掌握这一建模范式后，Z3 将成为你破解虚拟机、协议逆向、密码学约束等场景的高效利器。
