3

Z3 is a fantastic tool which helped me a lot! But sometimes I'm stuck on the binary code which implements custom If-logic. Recursive factorial function is good example of it:

def fact(x):
    if x == 1:
        return 1
    else:
        return x * fact(x - 1)

I'm aware of the fact Z3 python has If() function but it can only switch between two values.

Here is example of simple keygen-me which I wrote to illustrate this problem. Is there a way to solve it cleanly with Z3?

import sys

def fact(x):
    if x == 1:
        return 1
    else:
        return x * fact(x - 1)

def check_serial(s):

    for i in range(len(s)):
        if s[i] < 10:
            print("[!] poor serial number")
            exit(0)

    facts = [fact(s[i]) for i in range(len(s))]

    xor = 0
    for i in range(len(s)):
        xor = xor ^ facts[i]

    return xor


if len(sys.argv) != 9:
    print("[!] Usage: %s x x x x x x x x, where is number > 10" % sys.argv[0])
    exit(0)


nums = [int(x) for x in sys.argv[1:]]


if check_serial(nums) == 0x3fb4b7f405d4fb5e2a6740000:
    print("[+] serial number is valid, congratz!")
else:
    print("[!] serial number is invalid")
  • z3 is not very good with recursive function. You can find similar questions on SO – Paweł Łukasik Oct 17 at 14:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.