如何在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]的XOR和(ZeroExt(24, pwd[0])你的類型不匹配的位向量。

修復方法是在第一次出現時零擴展pwd[3]。