# Z3 Equation Solver - Bitmask Operation

0

After reverse engineering a program, I found the constraints.

I have to find two unsigned numbers such that:

``````x + y = 0xC0ED91BD
``````

and

``````x * y = Z
``````

In the original program, the multiplication of the numbers is performed using imul instruction.

Z should be such that when only the lower 32-bits of Z are checked, it should be less than 60.

``````Z & 0x00000000ffffffff < 60
``````

However, when I add the second equation as a constraint, z3 gives me an error.

Here's my code:

``````#! /usr/bin/python

from z3 import *
import sys

s = Solver()
result = int(sys.argv[1], 16)

x = Int('x')
y = Int('y')

s.add(x > 0, y > 0)
s.add((x * y) & 0x00000000ffffffff < 60)

while s.check() == sat:
print s.model()
s.add(Or(x != s.model()[x], y != s.model()[y]))
``````

Updated:

Here is the code based on the recommended solution:

``````#! /usr/bin/python

from z3 import *
import sys

s = Solver()
x = BitVec('x', 32)
y = BitVec('y', 32)

result = BitVecVal(int(sys.argv[1], 16), 32)

s.add(x > 0, y > 0)

print s.check()
print s.model()
``````

The binary is 64-bit.

However, the multiplication operation is performed using 32-bit integers as shown below:

``````mov     edx, [rbp+var_14]
mov     eax, [rbp+var_10]
imul    eax, edx
``````

So if eax = 0x425a95e5 and edx = 0x7e92fbd8

Then after multiplication using imul instruction, eax will store: 0x00000038.

Both, the Carry Flag and Overflow Flag bits in the EFLAGS register will be set after it.

python
z3
z3py
asked on Stack Overflow Jan 18, 2019 by Neon Flash • edited Jan 18, 2019 by Neon Flash

1

The issue here is that you have declared `x` and `y` to be arbitrarily wide integers, as opposed to bit-vectors of a fixed length. Simply change your declarations to match what the underlying bit-size should be. Assuming you want your arithmetic to be done in 32 bits, you'd say:

``````x = BitVec('x', 32)
y = BitVec('y', 32)
``````

instead. You should also declare `result` similarly:

``````result = BitVecVal(int(sys.argv[1], 16), 32)
``````

Once you make these changes, your program should work just fine.

Note that in this case masking with `0x00000000ffffffff` isn't really necessary; since the numbers are already 32-bits wide. You only need to keep it if your `x` and `y` are larger; say 64 bits.

With the above changes, I get the following output when I run your program and call it with `0xC0ED91BD`:

``````[y = 2123561944, x = 1113232869]
[y = 1440310864, x = 1796483949]
[y = 1171875408, x = 2064919405]
... many other lines ..
``````

This might look confusing, as the numbers seem to be larger than what you think they should be. But remember that arithmetic over bitvectors is done modulo `2^n` where `n` is the bit-size, so the results are actually correct:

``````>>> 2123561944 + 1113232869 % 2**32 == 0xC0ED91BD
True
>>> 2123561944 * 1113232869 % 2**32 < 60
True
``````

etc.

answered on Stack Overflow Jan 18, 2019 by alias • edited Jan 18, 2019 by alias

User contributions licensed under CC BY-SA 3.0