Well, I screwed up. I was only able to solve only one rev chall, their warmup. I guess it’s normal for a n00b like me, though.
The Large Cherries
We’re given a file called Lao-Tzu.
There’s a ptrace at the very top, so if you bypass it, you will see that:
It asks for two kinds of inputs, and for the first time, it asks for 9 characters and 10 characters the second time.
The first input is sent to this function, called
The function essentially makes sure that certain conditions are met for input to input, even though the input asks for 9 characters. This is our key to solving this chall.
from z3 import Solver, Xor, BitVec a = [BitVec('a%s' % i,64 ) for i in range(9)] s = Solver() s.add(a + a == 0xab) s.add(a == 0x37) s.add(a ^ a == 0x5d) s.add(a - a == 5) s.add(a + a == 0xa2) s.add(a == a) s.add(a == 0x30) s.add(a == 0x7a) s.check() m = s.model() print(s.model()) b=  for i in range(8): b.append(chr(int(m[a[i]].as_string()))) c = ''.join(b) print(c)
Now, this piece of code gives out
t0m7r00z, which is only 8 characters. This will be important later.
The second piece of input is a 10 character input, that checks if all of the characters add up to
660. That happens to be the sum of digital sum of
Therefore, we need to add something extra to the mix. This character can be quite literally anything, and I just typed
t0m7r00za as both inputs.