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

Question

我正在尝试找出隐藏在二进制文件中的注册机算法的密码。所以，我从程序集中提取公式并翻译（正确地，希望）在一个小的 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] 第一次出现时零扩展。

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

Howt to use properly ZeroExt(n,a) in a Z3py formula?

smt

z3

z3py