I initially encountered this problem in the SpaceHeroes CTF competition. Upon first glance, it was clear that there was no way I would solve this with mental math or like a standard equation. Giving more context to this problem, the user had to input three numbers passed into this function.
Function Decompiled with Ghidra:
int FUN_001012ce(int param_1,int param_2,int param_3) {
return (param_1 + param_2 + param_3 << ((byte)(param_1 % param_2) & 0x1f)) / (int)((2 << ((byte)param_1 & 0x1f) ^ 3U) * param_3);
}If the function's output is not equal to 0xa4c570 or 10,798,448 in decimal format, the binary will exit, and we won't get the flag. I immediately went to Google, looking for a "multi-variate bitwise equation solver," to no avail.
As I continued looking for an online equation solver that could handle bitwise shifts and xor operations, I kept seeing occasional references to the "Z3 Theorem Solver" and decided to check it out. I quickly realized that Z3 existed to solve these problems, and it supported all the bit operators. I promptly dove into the python bindings for Z3 and spent about fifteen minutes learning the lay of the land. I quickly scrapped together this code after taking another ten minutes to figure out that I had to represent my numerical inputs as bit vectors rather than the int type in Z3.
from z3 import *
a = BitVec('a', 32)
b = BitVec('b', 32)
c = BitVec('c', 32)
num = ((a + b + c) << ((a % b) & 0x1F))
denom = (c \* ((2 << (a & 0x1F)) ^ 3))
equation = (num / denom)
s = Solver()
s.add(equation == 0xa4c570)
s.check()
m = s.model()
# print(m[a], m[b], m[c])
print(hex(s.model()[a].as_long()))
print(hex(s.model()[b].as_long()))
print(hex(s.model()[c].as_long()))And just like that, we had our solution to a seemingly tricky problem; Z3 had generated three perfect numbers instantaneously that had satisfied our conditions. There was only one more check to pass, submitting our three numbers at the seventeenth minute of the hour, which just required patience.