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) 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")