Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Using Z3 to solve crackme

Using Z3 to solve crackme

Julien Bachmann

November 05, 2015
Tweet

More Decks by Julien Bachmann

Other Decks in Technology

Transcript

  1. 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 !
  2. use case | standard crackme Pretty simple crackme No anti-reverse

    engineering protections Need to have id/serial tuple that matches the criteria
  3. 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
  4. 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
  5. z3 | so what is it? Example usages solving Sudoku

    solving factorisation of large number into primes numbers
  6. z3 | so what is it? Example usages solving Sudoku

    solving factorisation of large number into primes numbers lame not sure about that one…
  7. 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
  8. z3 | types Constraints can only be applied to z3

    data types Numbers Int, Real, Bool Define multiples Ints Reals
  9. z3 | types Closest to our potentials cases CPU registers

    ! BitVec Extendable ZeroExt SignExt
  10. z3 | operators Standard ones +, -, *, ==, …

    RotateLeft, RotateRight Constraints And, Or ULT, UGT Distinct …
  11. 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
  12. 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