I am trying to find out the password of a keygen algorithm hidden in a binary. So, I extracted the formula from the assembly and translated (correctly, hopefully) in a small Python script to solve it:
#!/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)
Unfortunately, the ZeroExt(n,a) seems to produce the following error message:
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))
What did I do wrong and how to workaround this problem ?
NOTE: I changed the constants of the challenge to avoid to be easily found by searching for it (no cheating!). So, this problem might have no satisfiable solution...
It doesn't matter that you initialize the state vector to be 32-bits Z3 expressions. Once you overwrite state[0] to be the expression you supply, it is not 32 bits. It is instead just 8 bits. Also your bit-vector constants are truncated to 8 bits because of the bit-width of pwd[3].
So, the effect of:
state[0] = (pwd[3] ^ 0x1337) + 0x5eeded
is that state[0] contains a bit-vector that has size 8.
Then when you take the xor of state[0] and (ZeroExt(24, pwd[0]) you get the type mismatch.
A fix is to zero-extend pwd[3] in the first occurrence.