6

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.

4
  • Try help_simplify() - some of the options may do what you are looking for. Feb 2, 2014 at 21:45
  • I already tried several of these tactics (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 !
    – perror
    Feb 2, 2014 at 21:49
  • 1
    The question isn't very clear. What does "efficiently" mean, and what makes simplify "inefficient"? Feb 2, 2014 at 23:49
  • You're right. I meant more efficiently than a brute-force approach where you check all formula against the one you are investigating.
    – perror
    Feb 3, 2014 at 6:31

1 Answer 1

6

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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.