Given a simple shift-and-XOR operation, where 'input' is symbolic:
input = BitVec('input',32)
feedback = 0x8049d30
shiftreg = input ^ feedback
shiftreg = 0xffffffff & ((shiftreg << 8) | (shiftreg >> 24))
shiftreg = shiftreg ^ 0xcafebabe
s = Solver()
s.add(shiftreg == 0x804a008)
s.check()
# unsat
We are told that this equation is not solvable. If printed, s contains:
[4294967295 &
((input ^ 134520112) << 8 | (input ^ 134520112) >> 24) ^
3405691582 ==
134520840]
However, I can trivially create an example that solves this equation for 'input'.
want = 0x804a008
want ^= 0xcafebabe
want = 0xffffffff & ((want >> 8) | (want << 24))
want ^= 0x8049d30
print hex(want)
# 0xbec6672a
Entering our solution into Z3's equation, we see that we can satisfy it.
input = 0xbec6672a
[4294967295 &
((input ^ 134520112) << 8 | (input ^ 134520112) >> 24) ^
3405691582 ==
134520840]
# True
Why can Z3 not find this solution?
It turns out that in Z3, the shift operators are arithmetic shifts rather than logical shifts.
This means that a right shift >> is filled with the sign bit, rather than filled with zeroes.
You must use the Logical Shift Right (LShR) function in order to get normal behavior.
input = BitVec('input',32)
feedback = 0x8049d30
shiftreg = input ^ feedback
shiftreg = (shiftreg << 8) | LShR(shiftreg, 24)
shiftreg = shiftreg ^ 0xcafebabe
s = Solver()
s.add(shiftreg == 0x804a008)
s.check()
hex(s.model()[input].as_long())
# 0xbec6672a
In this particular example, the shift operation is actually a rotate. Z3 has a mechanism for doing the rotate directly (in this case, it would be RotateLeft(shiftreg, 8).