Z3pyの式でZeroExt（n、a）を正しく使うには？

Question

私はバイナリで隠されたkeygenアルゴリズムのパスワードを調べようとしています。だから、私は、アセンブリから式を抽出し、それを解決するために、小さなPythonスクリプトで（正しく、うまくいけば）翻訳：

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)) 

：

#!/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)は、次のエラーメッセージを生成しているようです

私は何が間違っていましたか？そしてこの問題を回避する方法は？

NOTE：チャレンジの定数を変更して、それを検索することで簡単に見つけられないようにしました（不正行為ではありません）。したがって、この問題には充分な解決策がない可能性があります。

Answer 1

状態ベクトルを32ビットZ3式に初期化する必要はありません。 state[0]を指定した式に上書きすると、32ビットではありません。それはちょうど8ビットです。また、ビット幅がpwd[3]のため、ビットベクトル定数は8ビットに切り捨てられます。

だから、の効果：

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

はstate[0]あなたはstate[0]のXORを取り、(ZeroExt(24, pwd[0])とき、あなたは型の不一致を取得するサイズ8

を持っているビットのベクトルが含まれていることです。

修正点は、最初のオカレンスでpwd[3]をゼロ拡張することです。