How to efficiently simplify obfuscated formula in QF_BV logic with Z3?

Question

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.

Answer 1

Z3 is an SMT solver. Its job is to decide the satisfiability of formulas passed in by a user, where the formulas may mix terms from the various theories that Z3 supports. Coincidentally, in order to make its own job easier by producing a "simpler" formula than the one passed in by the user, it implements a simplifier which is not very sophisticated technologically and largely consists of term rewriting rules.

Although the user could pose a query regarding the equivalence of two expressions, Z3's only involvement would be to solve the formula. I.e. Z3 will not generate candidates for you. It is your job as the user to provide the candidates and query an SMT solver as to their satisfiability.

In general, synthesizing functions is a challenging task in program synthesis. These queries are naturally posed in second-order logic, but modern SMT solvers support only restrictions of first-order logic. To sidestep this problem, some published work takes the route of eliminating most candidates from consideration ahead of time, thereby keeping the number of equivalence queries small. See for example this paper or this one. Another approach is to specify a template describing what the candidate functions are allowed to look like; a simple example is this paper. These approaches keep the formula to first-order logic, or even quantifier-free.

In general, you should research program synthesis.