4 ms·

How was Z3 useful for CTFs ?

• 0xdada 7y ago
  You can solve many keygen type reverse engineering challenges with z3.
  • viraptor 7y ago
    I'd be interested in reading about it. Do you convert the core algorithm into solver rules to find any solution? Or something more complex?
    • 0xdada 7y ago
      Yes. It basically turns a reverse engineering task back into regular "forward" engineering, except you are programming with z3's symbolic variables. Here is an example: https://anee.me/solving-a-simple-crackme-using-z3-68c55af7f7b1 https://anee.me/solving-a-simple-crackme-using-z3-68c55af7f7...