daily pastebin goal
33%
SHARE
TWEET

Untitled

a guest Apr 11th, 2016 2,310 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. # (c) 04/11/2016, Rolf Rolles, Mobius Strip Reverse Engineering
  2. import z3
  3. import struct
  4.  
  5. # XOR key for src.bin
  6. KEY_SECTOR = 0x37
  7.  
  8. # Counter position, as two words
  9. CNTLO      = 0
  10. CNTHI      = 0
  11.  
  12. # Symbolic names for array positions
  13. POS_CONST0 = 0
  14. POS_KEY0   = 1
  15. POS_KEY2   = 2
  16. POS_KEY4   = 3
  17. POS_KEY6   = 4
  18. POS_CONST2 = 5
  19. POS_NONCE0 = 6
  20. POS_NONCE2 = 7
  21. POS_CNTLO  = 8
  22. POS_CNTHI  = 9
  23. POS_CONST4 = 10
  24. POS_KEY8   = 11
  25. POS_KEY10  = 12
  26. POS_KEY12  = 13
  27. POS_KEY14  = 14
  28. POS_CONST6 = 15
  29.  
  30. # Constant values and their positions
  31. constvals = [ 0x7865, 0x646E, 0x2D32, 0x6574 ]
  32. constpos  = [ POS_CONST0, POS_CONST2, POS_CONST4, POS_CONST6 ]
  33.  
  34. # Key byte and word variables
  35. key_bytes = [ z3.BitVec('kb%d' % i,8) for i in xrange(8) ]
  36. key_words = [ None ]*len(key_bytes)
  37.  
  38. # Representation of key bytes as transformed words
  39. for i in xrange(len(key_bytes)):
  40.     hi = z3.ZeroExt(8,key_bytes[i]) << 9
  41.     lo = z3.ZeroExt(8,key_bytes[i]) + ord('z')
  42.     key_words[i] = hi | lo
  43.    
  44. # Position of key words within array
  45. keypos  = [ POS_KEY0, POS_KEY2, POS_KEY4, POS_KEY6, POS_KEY8, POS_KEY10, POS_KEY12, POS_KEY14 ]
  46.  
  47. # Initialize the modified Salsa.16-10 array (word-level values)
  48. def init_array(nonce0,nonce2,cntlo,cnthi):
  49.     initial_array = [None]*16
  50.     for i in xrange(len(constvals)):
  51.         initial_array[constpos[i]] = z3.BitVecVal(constvals[i],16)
  52.  
  53.     for i in xrange(len(key_words)):
  54.         initial_array[  keypos[i]] = key_words[i]
  55.    
  56.     initial_array[POS_NONCE0] = z3.BitVecVal(nonce0,16)
  57.     initial_array[POS_NONCE2] = z3.BitVecVal(nonce2,16)
  58.     initial_array[POS_CNTLO]  = z3.BitVecVal(cntlo, 16)
  59.     initial_array[POS_CNTHI]  = z3.BitVecVal(cnthi, 16)
  60.     return initial_array
  61.    
  62. # Input values to the Salsa round primitive
  63. salsa_steps = [
  64.   (4,0,12,7),
  65.   (8,4,0,9),
  66.   (12,8,4,13),
  67.   (0,12,8,18),
  68.  
  69.   (9,5,1,7),
  70.   (13,9,5,9),
  71.   (1,13,9,13),
  72.   (5,1,13,18),
  73.  
  74.   (14,10,6,7),
  75.   (2,14,10,9),
  76.   (6,2,14,13),
  77.   (10,6,2,18),
  78.  
  79.   (3,15,11,7),
  80.   (7,3,15,9),
  81.   (11,7,3,13),
  82.   (15,11,7,18),
  83.  
  84.   (1,0,3,7),
  85.   (2,1,0,9),
  86.   (3,2,1,13),
  87.   (0,3,2,18),
  88.  
  89.   (6,5,4,7),
  90.   (7,6,5,9),
  91.   (4,7,6,13),
  92.   (5,4,7,18),
  93.  
  94.   (11,10,9,7),
  95.   (8,11,10,9),
  96.   (9,8,11,13),
  97.   (10,9,8,18),
  98.  
  99.   (12,15,14,7),
  100.   (13,12,15,9),
  101.   (14,13,12,13),
  102.   (15,14,13,18),
  103. ]
  104.  
  105. # z3 representation of the Salsa.16 round primitive
  106. def step(arr,out,inl,inr,rotamt):
  107.     sum = z3.ZeroExt(16,arr[inl] + arr[inr])
  108.     rot = z3.RotateLeft(sum,rotamt)
  109.     arr[out] ^= z3.Extract(15,0,rot)
  110.  
  111. # Perform one Salsa.16 round
  112. def salsarnd(arr):
  113.     for rnd in salsa_steps:
  114.         step(arr,*rnd)
  115.  
  116. # Perform all 10 Salsa.16 rounds
  117. def salsa10(arr):
  118.     for i in xrange(10):
  119.         salsarnd(arr)
  120.  
  121. # Create solver object
  122. s = z3.SolverFor('QF_BV')
  123.  
  124. # Extract nonce words from the binary nonce data; create initial array
  125. with open("salsa10-nonce.bin", "rb") as f_nonce:
  126.     (n0,n2,n4,n6) = struct.unpack("HHHH", f_nonce.read())
  127.     initial = init_array(n0,n4,CNTLO,CNTHI)
  128.     init_copy = [ x for x in initial ]
  129.  
  130. # Extract ciphertext words from the binary sector data
  131. with open("salsa10-src.bin", "rb") as f_src:
  132.     srcbytes   = bytearray(f_src.read())
  133.     z3srcwords = [ None ] * len(initial)
  134.     for i in xrange(len(initial)):
  135.         lo = (srcbytes[4*i]   ^ KEY_SECTOR)
  136.         hi = (srcbytes[4*i+1] ^ KEY_SECTOR) << 8
  137.         z3srcwords[i] = z3.BitVecVal(hi | lo,16)
  138.  
  139. # Specify constraints on key bytes
  140. for k in key_bytes:
  141.     s.add(k != ord('O'))
  142.     s.add(k != ord('I'))
  143.     s.add(k != ord('l'))
  144.     s.add(z3.Or(z3.And(k >= 0x31,k <= 0x39),z3.And(k >= 0x61,k <= 0x78),z3.And(k >= 0x41,k <= 0x58)))
  145.  
  146. # Perform the Salsa.16 operation
  147. salsa10(initial)
  148.  
  149. # Specify constraints on outputs
  150. for i in xrange(len(initial)):
  151.     s.add((init_copy[i] + initial[i]) == z3srcwords[i])
  152.  
  153. # Check SAT, print solution if so
  154. if s.check() == z3.sat:
  155.     m = s.model()
  156.     keybytes = map(lambda k: chr(m[k].as_long()), key_bytes)
  157.     print 'x'.join(keybytes)
  158.  
  159. else:
  160.     print "UNSAT!"
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top