CODEWITHSUNDEEP
pythonz3z3py
Neon Flash
Neon Flash

Reputation: 3233

Using z3 where constraint depends on output of function

I want to use z3 to solve this case. The input is a 10 character string. Each character of the input is a printable character (ASCII). The input should be such that when calc2() function is called with input as a parameter, the result should be: 0x0009E38E1FB7629B.

How can I use z3py in such cases?

Usually I would just add independent equations as a constraint to z3. In this case, I am not sure how to use z3.

def calc2(input):
    result = 0

    for i in range(len(input)):
        r1 = (result << 0x5) & 0xffffffffffffffff
        r2 = result >> 0x1b
        r3 = (r1 ^ r2)

        result = (r3 ^ ord(input[i]))

    return result

if __name__ == "__main__":
        input = sys.argv[1]
        result = calc2(input)

        if result == 0x0009E38E1FB7629B:
             print "solved"

Update: I tried the following however it does not give me correct answer:

from z3 import *

def calc2(input):
    result = 0

    for i in range(len(input)):
        r1 = (result << 0x5) & 0xffffffffffffffff
        r2 = result >> 0x1b
        r3 = (r1 ^ r2)

        result = r3 ^ Concat(BitVec(0, 56), input[i])


    return result

if __name__ == "__main__":
    s = Solver()
    X = [BitVec('x' + str(i), 8) for i in range(10)]

    s.add(calc2(X) == 0x0009E38E1FB7629B)

    if s.check() == sat:
        print(s.model())

Upvotes: 1

Views: 1135

Answers (2)

alias
alias

Reputation: 30525

I hope this isn't homework, but here's one way to go about it:

from z3 import *

s = Solver()

# Input is 10 character long; represent with 10 8-bit symbolic variables
input = [BitVec("input%s" % i, 8) for i in range(10)]

# Make sure each character is printable ASCII, i.e., between 0x20 and 0x7E
for i in range(10):
  s.add(input[i] >= 0x20)
  s.add(input[i] <= 0x7E)

def calc2(input):

    # result is a 64-bit value
    result = BitVecVal(0, 64)

    for i in range(len(input)):
        # NB. We don't actually need to mask with 0xffffffffffffffff
        # Since we explicitly have a 64-bit value in result.
        # But it doesn't hurt to mask it, so we do it here.
        r1 = (result << 0x5) & 0xffffffffffffffff
        r2 = result >> 0x1b
        r3 = r1 ^ r2

        # We need to zero-extend to match sizes
        result = r3 ^ ZeroExt(56, input[i])

    return result


# Assert the required equality
s.add(calc2(input) == 0x0009E38E1FB7629B)

# Check and get model
print s.check()
m = s.model()

# reconstruct the string:
s = ''.join([chr (m[input[i]].as_long()) for i in range(10)])
print s

This prints:

$ python a.py
sat
L`p:LxlBVU

Looks like your secret string is

"L`p:LxlBVU"

I've put in some comments in the program to help you with how things are coded in z3py, but feel free to ask for clarification. Hope this helps!

Getting all solutions

To get other solutions, you simply loop and assert that the solution shouldn't be the previous one. You can use the following while loop after the assertion:

while s.check() == sat:
   m = s.model()
   print ''.join([chr (m[input[i]].as_long()) for i in range(10)])
   s.add(Or([input[i] != m[input[i]] for i in range(10)]))

When I ran it, it kept going! You might want to stop it after a while.

Upvotes: 1

Nuno Lopes
Nuno Lopes

Reputation: 868

You can encode calc2 in Z3. you'll need to unroll the loop for 1,2,3,4,..,n times (for n = max input size expected), but that's it. (You don't actually need to unroll the loop, you can use z3py to create the constraints)

Upvotes: 0

Related Questions