text: .
  import sys import struct # the input string s = sys.argv[1] # pad the string upto four bytes if it's less (which is the case # for the last part, which consists of only three bytes) num = struct.unpack('I', s + '\x00' * (4 - len(s)))[0] # shift a bit, xor with deadbeef, and add deadbeef print ((((num << 0x15) | (num >> 0x15)) ^ 0xdeadbeef) + 0xdeadbeef) % 2**32
  At this point we can either make a bruteforcer ourselves, or let Z3 do the
  dirty job. Sometime ago Rolf Rolles answered a fun question by providing a
  theorem-prover based solution. This small answer can be found here:
  Based on this solution we made our own Z3 solver. First one must learn a bit
  about SMT solvers; as we operate the integers on a bit-level here, we must use
  BitVectors. These BitVectors can be pretty much any size, but here we’ll use
  32 bit-sized BitVectors as our required numbers are 32-bits. Our first attempt
  in making the Z3 solver was based on the LIB-SMT2 library; basically one
  submits a .smt2 file to the z3 binary and it gives a result in return.
  Our first .smt2 file looked like the following. (Note that #xdeadbeef
  represents a hexadecimal value which will be interpreted as BitVector.)
  (set-logic BV) (declare-const input (_ BitVec 32)) (assert (= ; algorithm from the binary (bvadd (bvxor (bvor (bvshl input (_ bv21 32)) (bvashr input (_ bv21 32))) #xdeadbeef) #xdeadbeef) ; magic value from the binary #x2f5b7b03)) (check-sat) (get-model)
  So what happens here? First we declared our input variable, which is a 32-bit
  BitVector. Then we make an assert that the following condition(s) must be met.
  In this condition, we encode our desired algorithm into the LIB-SMT2
  equivalent. Our input is first shifted, using *bvshl* and *bvshr*. These are
  the BitVector variants of shl (shift left) and shr (shift right.) The results
  of these two values are then or’d, using bvor (again, the BitVector version of
  *or*.) This value is then xor’d with 0xdeadbeef, and finally 0xdeadbeef is
  added to it. After these operations, the output value is compared to a magic
  value which we got from the binary. Namely in a compare instruction which
  compared our value to the magic value.
  By asserting Z3 that the shuffled input value must match the given magic value
  it will then go on a relatively short journey to find our value. And yes,
  after a few dozen milliseconds it finds a candidate:
  $ z3.exe cone.smt2 sat (model (define-fun input () (_ BitVec 32) #x5f600470) )
  As we can see, the output is 0x5f600470. However, we’ll have to encode this
  32-bit number as 4 characters, and earlier we saw in the binary that
  (logically) only readable characters are allowed. Hence this value will be
  discarded (as it contains \x04.) We modified our solver a bit to discard
  various hardcoded values (these were added on-demand.) Finally, to get a
  correct solution for the first magic value we got the following solver.
  (set-logic BV) (declare-const input (_ BitVec 32)) (assert (and ; input may not match any of the following values (not (= input #x5f600470)) (not (= input #x5f600c70)) (not (= input #x5f601470)) (not (= input #x5f601c70)) ; compute a correct input value (= (bvadd (bvxor (bvor (bvshl input (_ bv21 32)) (bvashr input (_ bv21 32))) #xdeadbeef) #xdeadbeef) #x2f5b7b03))) (check-sat) (get-model)
  $ z3.exe cone.smt2 sat (model (define-fun input () (_ BitVec 32) #x5f602470) )
  As you can see, it’s pretty ugly, but it does the job; the output variable is
  0x5f602470, which is accepted by the cone binary (as each character represents
  a readable one.) From here on we kept adding values to the blacklist as we got
  four bad values for every magic value we found in the binary (it turns out
  there were nine magic values.) After running all the magic values through our
  solver we got a solution that surprised the organizers, so that’s nice 🙂
  19:28:18 <skier_> i can haz readable flag ;P 19:28:36 <skier_> p$`_s%`d_0`lp7`m_!`_a7`ta#`_m!`hin` 19:28:38 <skier_> lol 19:28:46 <ricky> Woah, that's accepted by the new one? 19:28:49 <skier_> ya
  Our final solution in LIB-SMT2 can be found on the end of this blogpost.
  However, we’ll now dive into the Python bindings of Z3, which makes life a lot
  cooler and easier.
  First we take a function from the following StackOverflow post:. The function presented in this
  answer basically takes a set of conditions to be met and then adds the results
  retrieved from the solver to the blacklist until the solver can’t find any new
  solutions. This way we can get multiple/all solutions from the solver (which
  is literally impossible with LIB-SMT2.)
  That said, we have to re-implement our conditions in Python. First we define
  an input BitVector and a temporary BitVector (which really only splits the
  algorithm up into two smaller conditions), then we define the two conditions,
  and finally we run the results through a checker (i.e., we run each 8-bit
  value of the result through a checker to check if it’s a valid character.)
  This results in the following code. Note that the Z3 Python bindings do quite
  some operator overloading which allows us to do “bitvector << val" etc. [code lang="python"] import random import struct from z3 import Solver, BitVecs, BitVecVal, And, Or from z3 import sat, is_array, Z3Exception, Z3_UNINTERPRETED_SORT # Return all the models of formula list of formulas F def get_models(F): result = [] s = Solver() s.add(F) while True: if s.check() == sat: m = s.model() result.append(m) # Create a new constraint the blocks the current model block = [] for d in m: # d is a declaration if d.arity() > 0: raise Z3Exception( "uninterpreted functions are not suppported") # create a constant from declaration c = d() if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT: raise Z3Exception( "arrays and uninterpreted sorts are not supported") block.append(c != m[d]) s.add(Or(block)) else: return result # this function checks whether each character is either an # underscore or lowercase ascii def is_lower_underscore(x): return Or(x == 0x5f, And(x >= 0x61, x <= 0x7a)) def get_combinations(magic, checker): # input and temporary bitvectors i, tmp = BitVecs('input temp', 32) F = [ # first condition - temp equals the shifted input tmp == ((i << BitVecVal(21, 32)) | (i >> BitVecVal(21, 32))), # second condition (0xdeadbeef + (0xdeadbeef ^ tmp)) == magic, # check if each character is readable checker((i >> 0) & 0xff), checker((i >> 8) & 0xff), checker((i >> 16) & 0xff)] # the last magic value only has three input characters, so.. if magic != 0xf23b7ddb: F.append(checker((i >> 24) & 0xff)) # get all models and retrieve the 32bit combinations # bit hacky, but that's Z3. return [x[x[0]].as_long() for x in get_models(F)] # each magic value from the binary l = [0x2f5b7b03, 0x4f7b7cbb, 0xb3fb7c7b, 0x0f5b7c73, 0xd3fb7b03, 0x113b7c3b, 0x913b7b03, 0xd1bb7c9b, 0xf23b7ddb] combinations = [get_combinations(x, is_lower_underscore) for x in l] # print 50 random keys for _ in xrange(50): print ''.join(struct.pack('I', random.choice(combinations[x])) for x in xrange(len(combinations))) [/code] [code lang="bash"] $ python cone.py pdj_smod_pglp_zm_yo_awctakg_mayhivx pdk_smdd_xslpgnm_im_a_ktakf_miphifc pdc_smxd_phlpglm_ai_aobtacr_mayhivf pdj_sehd_hnlp_jm_ig_agqtakh_mixhins [..] [/code] Well, that was pretty cool. Following is also the final LIB-SMT2 file. Note that you have to uncomment a magic value if you want a solution for that one (and can only have one uncommented magic value at a time.) [code] (set-logic BV) (declare-const input (_ BitVec 32)) (assert (and (not (= input #x5f600470)) (not (= input #x5f600c70)) (not (= input #x5f601470)) (not (= input #x5f601c70)) (not (= input #x64600573)) (not (= input #x64600d73)) (not (= input #x64601573)) (not (= input #x64601d73)) (not (= input #x6c60005f)) (not (= input #x6c60085f)) (not (= input #x6c60105f)) (not (= input #x6c60185f)) (not (= input #x6c60205f)) (not (= input #x6d600770)) (not (= input #x6d600f70)) (not (= input #x6d601770)) (not (= input #x6d601f70)) (not (= input #x6d602770)) (not (= input #x5f60015f)) (not (= input #x5f60095f)) (not (= input #x5f60115f)) (not (= input #x5f60195f)) (not (= input #x74600761)) (not (= input #x74600f61)) (not (= input #x74601761)) (not (= input #x74601f61)) (not (= input #x74602761)) (not (= input #x00606669)) (= (bvadd (bvxor (bvor (bvshl input (_ bv21 32)) (bvashr input (_ bv21 32))) #xdeadbeef) #xdeadbeef) ; #x2f5b7b03))) ; #x4f7b7cbb))) ; #xb3fb7c7b))) ; #x0f5b7c73))) ; #xd3fb7b03))) ; #x113b7c3b))) ; #x913b7b03))) ; #xd1bb7c9b))) #xf23b7ddb))) (check-sat) (get-model) [/code]
  sorry, stupid question, but what is z3 ?
  Thanks.
  Thanks a lot for publishing this writeup!
  How did you get the “magic instruction trace”?
  Z3 is a powerful theorem prover developed by Microsoft Research.
  Check it out at:
  Great writeup. I was also wondering about the “magic” trace. Was it manual or tool-assisted?