Z3py 수식에서 ZeroExt (n, a)를 올바르게 사용하는 방법?

Question

바이너리에 숨겨진 keygen 알고리즘의 암호를 찾으려고합니다. 그래서, 나는 어셈블리에서 공식을 추출하고이를 해결하기 위해 작은 파이썬 스크립트 (정확하게, 희망) 번역 :

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) 다음과 같은 오류 메시지를 생성하는 것

내가 뭘 잘못했는데이 문제를 해결하는 방법은 무엇입니까?

참고 : 도전 과제의 상수를 변경하여 쉽게 찾을 수 없도록했습니다 (속임수가 아님!). 그래서,이 문제는 만족스러운 해결책이 없을 수도 있습니다 ...

Answer 1

상태 벡터를 32 비트 Z3 표현식으로 초기화해도 상관 없습니다. state[0]을 공급 한 표현식으로 덮어 쓰면 32 비트가 아닙니다. 대신 단지 8 비트입니다. 또한 비트 - 너비가 pwd[3]이기 때문에 비트 - 벡터 상수가 8 비트로 잘립니다.

그래서, 효과 :

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

는 state[0] 당신이 유형 불일치를 얻을 수 (ZeroExt(24, pwd[0])state[0]의 XOR을 때 그 다음 크기를 8

을 가진 비트 벡터를 포함하고 있다는 점이다.

첫 번째 발생시 pwd[3]의 제로 확장을 수정했습니다.