如何在 Z3py 公式中正确使用 ZeroExt(n,a)？

Question

我正在尝试找出隐藏在二进制文件中的 keygen 算法的密码。因此，我从程序集中提取公式并（希望正确地）翻译成一个小的 Python 脚本来解决它：

#!/usr/bin/env python
from z3 import *

# Password initialization
pwd = BitVecs('pwd0 pwd1 pwd2 pwd3 pwd4 pwd5', 8)

# Internal states
state = BitVecs('state0 state1 state2 state3 state4 state5 state6', 32)

# Building the formula
state[0] = (pwd[3] ^ 0x1337) + 0x5eeded
for i in range(6):
    state[i+1] = (ZeroExt(24, pwd[i]) ^ state[i]) % 0xcafe

# Solving the formula under constraint
solve(state[6] == 0xbad1dea)

不幸的是，ZeroExt(n,a) 似乎会产生以下错误消息：

Traceback (most recent call last):
  File "./alt.py", line 13, in <module>
    state[i+1] = (ZeroExt(24, pwd[i]) ^ state[i]) % 0xcafe
  File "/usr/lib/python2.7/dist-packages/z3.py", line 3115, in __xor__
    return BitVecRef(Z3_mk_bvxor(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
  File "/usr/lib/python2.7/dist-packages/z3core.py", line 1743, in Z3_mk_bvxor
    raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
z3types.Z3Exception: Argument (bvadd (bvxor pwd3 #x37) #xed) at position 1 does not match declaration (declare-fun bvxor ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))

我做错了什么以及如何解决这个问题？

注意：我更改了挑战的常量以避免通过搜索轻松找到它（没有作弊！）。所以，这个问题可能没有令人满意的解决方案......

Answer 1

将状态向量初始化为 32 位 Z3 表达式并不重要。一旦您覆盖 state[0] 成为您提供的表达式，它就不是 32 位。相反，它只有 8 位。由于pwd[3] 的位宽，您的位向量常量也被截断为 8 位。

所以，效果：

     state[0] = (pwd[3] ^ 0x1337) + 0x5eeded

state[0] 是否包含大小为 8 的位向量。

然后，当您对 state[0] 和 (ZeroExt(24, pwd[0]) 进行异或运算时，您会得到类型不匹配。

解决方法是在第一次出现时将 pwd[3] 零扩展。