Take the 2-minute tour ×
Reverse Engineering Stack Exchange is a question and answer site for researchers and developers who explore the principles of a system through analysis of its structure, function, and operation. It's 100% free, no registration required.

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.

share|improve this question
    
Try help_simplify() - some of the options may do what you are looking for. –  Vitaly Osipov Feb 2 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 at 21:49
1  
The question isn't very clear. What does "efficiently" mean, and what makes simplify "inefficient"? –  Rolf Rolles Feb 2 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 at 6:31
add comment

1 Answer

up vote 6 down vote accepted

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.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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