I would like to know if there are efficient ways to simplify arithmetic formula expression over bit-vectors with Microsoft Z3. But, first, I would like to explain a bit the problem. Lets start with an example:
x + y == (x ^ y) + 2 * (x & y)
Both x + y
and (x ^ y) + 2 * (x & y)
are, in fact, coding the addition over bit-vectors. Of course, the right hand formula is used to confuse a reverser when found in the binary program. I try to find tools and techniques to simplify the obfuscated formula and find the simpler form of the formula (left-hand).
For this, I looked at the Python interface of Z3, trying to see what I can get out of it. So, defining the obfuscated formula is done like this:
>>> from z3 import *
>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> fun1 = (x ^ y) + 2 * (x & y)
Now, lets try to simplify this function with the help of the built-in function simplify
:
>>> simplify((x ^ y) + 2 * (x & y))
(x ^ y) + 2*~(~x | ~y)
Not really convincing... But, lets try to prove the equivalence with x + y
:
>>> prove((x ^ y) + 2 * (x & y) == x + y)
proved
>>> prove((x ^ y) + 2 * (x & y) == x - y)
counterexample
[y = 2164268032, x = 2139094080]
I added a negative result to show that it is also possible to disqualify a formula.
So, if the simplify
function is not really convincing, it is still possible to try, in a brute-force manner to compare the unknown formula with a list of simpler and usual formula one after one. But, this way seems extremely inefficient to me. I guess I am missing some smarter algorithms to simplify formula.
I would like to know if there are some already existing tools or well-known techniques to perform in a more efficient manner than the brute-force approach. So, if someone has some hints or comments about this, it would be more than welcome.
help_simplify()
- some of the options may do what you are looking for.simplify(fun1, som=True)
), but with no success either. Maybe I missed the right set of tactics to use. If you have such a list, I would be happy to know your suggestion !simplify
"inefficient"?