hacktracking: # Pin and triton: Binary instrumentation and symbolic execution

# Pin and triton: Binary instrumentation and symbolic execution

Installation

$ wget 'http://old-releases.ubuntu.com/releases/14.04.0/ubuntu-14.04.1-server-amd64.iso' # kernel 3.x
$ # Install ubuntu server
$ # The installed server needs the following software
$ sudo apt-get install libboost1.55-dev
$ sudo apt-get install libpython2.7-dev
$ git clone https://github.com/Z3Prover/z3.git
$ cd z3
$ python scripts/mk_make.py --python
$ cd
$ wget 'http://www.capstone-engine.org/download/3.0.4/ubuntu-14.04/libcapstone3_3.0.4-0.1ubuntu1_amd64.deb'
$ wget 'http://www.capstone-engine.org/download/3.0.4/ubuntu-14.04/libcapstone-dev_3.0.4-0.1ubuntu1_amd64.deb'
$ sudo dpkg -i libcapstone3_3.0.4-0.1ubuntu1_amd64.deb
$ sudo dpkg -i libcapstone-dev_3.0.4-0.1ubuntu1_amd64.deb
$ # Pin version 71313
$ wget 'http://software.intel.com/sites/landingpage/pintool/downloads/pin-2.14-71313-gcc.4.4.7-linux.tar.gz'
$ tar xvzf pin-2.14-71313-gcc.4.4.7-linux.tar.gz
$ cd pin-2.14-71313-gcc.4.4.7-linux/source/tools
$ git clone https://github.com/JonathanSalwan/Triton.git
$ cd Triton
$ mkdir build
$ cd build
$ cmake -DPINTOOL=on ..
$ make
$ PATH=$PATH;~/pin-2.14-71313-gcc.4.4.7-linux/source/tools/Triton
$ cd ..
$ sysctl kernel.yama.ptrace_scope=0
$ triton ./src/examples/pin/ir.py /usr/bin/id

Challenge

$ wget 'https://raw.githubusercontent.com/black-bunny/First-hands-with-Triton/master/CrackMe.c'
$ gcc -o CrackMe CrackMe.c
$ cat CrackMe.py
import pintool
import triton

SNAPSHOT = False
ARGV1 = 0

MAIN = 0x4005bd
AVOID = [0x4006f2, 0x400714, 0x400727, 0x400744, 0x400760, 0x400782, 0x4007a4, 0x4007c3, 0x4007e7, 0x40082f, 0x400869, 0x40088e, 0x4008cf, 0x40096e]
TAKE = [0x40080b, 0x400910]
PASSWORD_SIZE = 11
SYMVAR_CONSTRAINTS = []
NUM_MANDATORY_PATHS = 0
LAST_INJECTED = ''

def superAnd(constraints):
 pc = triton.ast.equal(triton.ast.bvtrue(), triton.ast.bvtrue())
 for i in range(len(constraints)):
  pc = triton.ast.land(pc, constraints[i])
 return pc

def model2string(model):
 s = ''
 for i in range(PASSWORD_SIZE):
  try:
   s += chr(model[i].getValue())
  except:
   pass
 return s

def inject(address, data):
 for i, char in enumerate(data):
  pintool.setCurrentMemoryValue(address + i, ord(char))

def before(instruction):
 global SNAPSHOT
 global ARGV1
 global SYMVAR_CONSTRAINTS
 ia = instruction.getAddress()
 if ia == MAIN:
  if not SNAPSHOT:
   rsi = pintool.getCurrentRegisterValue(triton.REG.RSI)
   ARGV1 = pintool.getCurrentMemoryValue(rsi + 8, triton.CPUSIZE.REG)
   print 'rsi = ', rsi
   print 'ARGV1 = ', ARGV1

   offset = 0
   while offset < PASSWORD_SIZE:
    address = ARGV1 + offset
    pintool.setCurrentMemoryValue(address, ord('*'))
    symvar = triton.convertMemoryToSymbolicVariable(triton.MemoryAccess(address, triton.CPUSIZE.BYTE))
    SYMVAR_CONSTRAINTS.append(triton.ast.bvuge(triton.ast.variable(symvar), triton.ast.bv(0x20, 8)))
    SYMVAR_CONSTRAINTS.append(triton.ast.bvule(triton.ast.variable(symvar), triton.ast.bv(0x7e, 8)))
    offset +=1
   pintool.setCurrentMemoryValue(ARGV1 + offset, 0x0)

   print '[+] Symbolized %d bytes of memory at 0x%x' % (offset, ARGV1)
   print '[+] Taking snapshot'
   pintool.takeSnapshot()
   SNAPSHOT = True

def before_symproc(instruction):
 global NUM_MANDATORY_PATHS
 global LAST_INJECTED
 path_constraints = []
 ia = instruction.getAddress()

 if ia in TAKE:
  NUM_MANDATORY_PATHS += 1

 if (ia in AVOID) or (ia == 0x40080f and NUM_MANDATORY_PATHS != 1) or (ia == 0x400914 and NUM_MANDATORY_PATHS != 2):
  NUM_MANDATORY_PATHS = 0
  print '[+] Wrong password'
  pc = triton.getPathConstraints()
  for i in pc:
   if i.isMultipleBranches():
    for branch in i.getBranchConstraints():
     if branch['dstAddr'] in AVOID:
      path_constraints.append(triton.ast.lnot(branch['constraint']))
     if branch['dstAddr'] in TAKE:
      path_constraints.append(branch['constraint'])
  full_constraint = superAnd(SYMVAR_CONSTRAINTS + path_constraints)
  model = triton.getModel(triton.ast.assert_(full_constraint))
  s = model2string(model)
  LAST_INJECTED = s
  print '[+] Posible solution: ' + s + ' - ' + s.encode('hex')
  s += chr(0)
  print '[+] Injecting it and restoring snapshot'
  inject(ARGV1, s)
  triton.clearPathConstraints()
  pintool.restoreSnapshot()

 if ia == 0x400978:
  print '[+] Good password: ', LAST_INJECTED
  pintool.disableSnapshot()
  triton.clearPathConstraints()
  pintool.setCurrentRegisterValue(triton.REG.RIP, 0x400982)


def constantFolding(node):
 if node.isSymbolized():
  return node
 else:
  return triton.ast.bv(node.evaluate(), node.getBitvectorSize())

if __name__ == '__main__':
 triton.setArchitecture(triton.ARCH.X86_64)
 triton.enableSymbolicOptimization(triton.OPTIMIZATION.ALIGNED_MEMORY, True)
 triton.enableSymbolicOptimization(triton.OPTIMIZATION.ONLY_ON_SYMBOLIZED, True)

 #pintool.startAnalysisFromEntry()
 pintool.startAnalysisFromAddress(MAIN)

 triton.addCallback(constantFolding, triton.CALLBACK.SYMBOLIC_SIMPLIFICATION)
 pintool.insertCall(before, pintool.INSERT_POINT.BEFORE) # Before the instruction processing
 pintool.insertCall(before_symproc, pintool.INSERT_POINT.BEFORE_SYMPROC) # Before the symbolic processing
 pintool.runProgram()

$ triton CrackMe.py ./CrackMe -
rsi =  140734613450744
ARGV1 =  140734613456483
[+] Symbolized 11 bytes of memory at 0x7fff54a48663
[+] Taking snapshot
[+] Wrong password
[+] Posible solution: @@@ @@@@@ @ - 4040402040404040402040
[+] Injecting it and restoring snapshot
[+] Wrong password
[+] Posible solution: B*@!o@@A H; - 422a40216f40404120483b
[+] Injecting it and restoring snapshot
[+] Wrong password
[+] Posible solution: @@'@_H.@r\O - 404027405f482e40725c4f
[+] Injecting it and restoring snapshot
[+] Wrong password
[+] Posible solution: AQ%!$HD zR9 - 41512521244844207a5239
[+] Injecting it and restoring snapshot
[+] Wrong password
[+] Posible solution: Ui(1\GDAp^@ - 556928315c474441705e40
[+] Injecting it and restoring snapshot
[+] Wrong password
[+] Posible solution: 9\*(00 'xA& - 395c2a2830302027784126
[+] Injecting it and restoring snapshot
[+] Wrong password
[+] Posible solution: 7T"W8$$Bl9  - 37542257382424426c3920
[+] Injecting it and restoring snapshot
[+] Wrong password
[+] Posible solution: 0=#E$/oDy8% - 303d2345242f6f44793825
[+] Injecting it and restoring snapshot
[+] Wrong password
[+] Posible solution: 5G1x:)lgy@  - 354731783a296c67794020
[+] Injecting it and restoring snapshot
[+] Wrong password
[+] Posible solution: Gx/t0TRoqq( - 47782f743054526f717128
[+] Injecting it and restoring snapshot
[+] Wrong password
[+] Posible solution: or9t0NRo{kP - 6f723974304e526f7b6b50
[+] Injecting it and restoring snapshot
[+] Wrong password
[+] Posible solution: Tr;t0NRo}k5 - 54723b74304e526f7d6b35
[+] Injecting it and restoring snapshot
[+] Wrong password
[+] Posible solution: Tr!t0NRock5 - 54722174304e526f636b35
[+] Injecting it and restoring snapshot
[+] Good password:  Tr!t0NRock5

References

http://blackbunny.io/solving-a-crack-me-with-triton-and-pin-a-k-a-the-lazy-way/
https://github.com/black-bunny/First-hands-with-Triton

# Pin and triton: Binary instrumentation and symbolic execution

No comments: