Using Z3 to solve crackme

Transcript

1. Using z3 to solve crackme Julien Bachmann @milkmix_
2. how | irc, con and ctf Some have been talking about it for a long time Lately : Defcon’15 CTF fuckup challenge “The flag is: z3 always helps” solved by teammate using… z3 !
3. use case | standard crackme Pretty simple crackme No anti-reverse engineering protections Need to have id/serial tuple that matches the criteria
4. use case | standard crackme
5. use case | reverse and reimplement Inputs should be alphanumeric strings between 6 and 9 characters All distinct Sums of both strings characters should be equal compute_serial == compute_id Serial should have increasing order at even positions, decreasing at odd ones
6. z3 | so what is it? z3 is an SMT solver Satisfiability Modulo Theory an extension of SAT solvers give it an equation and it can tell you if solvable or not even give you an answer not necessarily the best one
7. z3 | so what is it? Example usages solving Sudoku solving factorisation of large number into primes numbers
8. z3 | so what is it? Example usages solving Sudoku solving factorisation of large number into primes numbers lame not sure about that one…
9. z3 | so what is it? For me it is more an Cyber Oracle honestly, I didn’t looked at all the theory and maths behind
10. z3 | installation Open sourced by Microsoft yeah, for real ! https://github.com/Z3Prover/z3
11. z3 | types Constraints can only be applied to z3 data types Numbers Int, Real, Bool Define multiples Ints Reals
12. z3 | types Closest to our potentials cases CPU registers ! BitVec Extendable ZeroExt SignExt
13. z3 | types Warning ! Int are infinite numbers BitVec are wrapping, like registers
14. z3 | operators Standard ones +, -, *, ==, … RotateLeft, RotateRight Constraints And, Or ULT, UGT Distinct …
15. z3 | solver The class you will be using the most add : add a constraint to the equation push/pop : store current state of the constraints prove : check if given equation is always true check : validate if solution exists model : if solvable, return a solution simplify : simplify current equation
16. z3 | solver
17. crackme | time to solve it
18. crackme | time to solve it
19. conclusion | awesome Quite useful tool when brute force would take too long problem can easily be put in the form of equations Can be applied to auto-ROP to solve constraints on registers concolic execution (symbolic+concrete) check Quarkslab Triton