Z3python Xor Sum?

I'm currently trying to solve some equation with z3python, and I am coming across a situation I could not deal with. I need to xor certain BitVecs with specific non ascii char valu

Solution 1:

There are two problems in your code.

• Xor is for Bool values only; for bit-vectors simply use ^
• Use the function ord to convert characters to integers before passing to xor

You didn't give your full program (which is always helpful!), but here's how you'd write that section in z3py as a full program:

from z3 import *

solver = Solver()
KEY_LEN = 10

pbInput = [BitVec("c_{}".format(i), 8) for i inrange(KEY_LEN)]
password = "\xff\xff\xde\x8e\xae"
solver.add((pbInput[0] ^ ord(password[0])) + (pbInput[3] ^ ord(password[3])) == 300)

print solver.check()
print solver.model()

This prints:

sat
[c_3 = 0, c_0 = 97]

(I gave the variables better names to distinguish more properly.) So, it's telling us the solution is:

>>>(0xff ^ 97) + (0x8e ^ 0)
300

Which is indeed what you asked for.