1#!/usr/bin/env python 2## -*- coding: utf-8 -*- 3## 4## Jonathan Salwan - 2016-08-02 5## 6## Description: Solution of the r100 challenge from the Defcamp 2015 CTF. 7## In this solution, we fully emulate the CheckSolution() function and we 8## solve each branch to go through the good path. 9## 10## Output: 11## 12## $ python ./solve.py 13## [...] 14## 400784: movsx eax, al 15## 400787: sub edx, eax 16## 400789: mov eax, edx 17## 40078b: cmp eax, 1 18## [+] Asking for a model, please wait... 19## [+] Symbolic variable 00 = 43 (C) 20## [+] Symbolic variable 01 = 6f (o) 21## [+] Symbolic variable 02 = 64 (d) 22## [+] Symbolic variable 03 = 65 (e) 23## [+] Symbolic variable 04 = 5f (_) 24## [+] Symbolic variable 05 = 54 (T) 25## [+] Symbolic variable 06 = 61 (a) 26## [+] Symbolic variable 07 = 6c (l) 27## [+] Symbolic variable 08 = 6b (k) 28## [+] Symbolic variable 09 = 65 (e) 29## [+] Symbolic variable 10 = 72 (r) 30## [+] Symbolic variable 11 = 73 (s) 31## 40078e: je 0x400797 32## 400797: add dword ptr [rbp - 0x24], 1 33## 40079b: cmp dword ptr [rbp - 0x24], 0xb 34## 40079f: jle 0x40072d 35## 4007a1: mov eax, 0 36## 4007a6: pop rbp 37## 4007a7: ret 38## [+] Emulation done. 39## 40 41from __future__ import print_function 42from triton import ARCH, TritonContext, Instruction, MODE, MemoryAccess, CPUSIZE 43 44import os 45import sys 46 47Triton = TritonContext() 48 49 50# Emulate the CheckSolution() function. 51def emulate(pc): 52 astCtxt = Triton.getAstContext() 53 print('[+] Starting emulation.') 54 while pc: 55 # Fetch opcode 56 opcode = Triton.getConcreteMemoryAreaValue(pc, 16) 57 58 # Create the Triton instruction 59 instruction = Instruction() 60 instruction.setOpcode(opcode) 61 instruction.setAddress(pc) 62 63 # Process 64 Triton.processing(instruction) 65 print(instruction) 66 67 # 40078B: cmp eax, 1 68 # eax must be equal to 1 at each round. 69 if instruction.getAddress() == 0x40078B: 70 # Slice expressions 71 rax = Triton.getSymbolicRegister(Triton.registers.rax) 72 eax = astCtxt.extract(31, 0, rax.getAst()) 73 74 # Define constraint 75 cstr = astCtxt.land([ 76 Triton.getPathPredicate(), 77 astCtxt.equal(eax, astCtxt.bv(1, 32)) 78 ]) 79 80 print('[+] Asking for a model, please wait...') 81 model = Triton.getModel(cstr) 82 for k, v in list(sorted(model.items())): 83 value = v.getValue() 84 Triton.setConcreteVariableValue(Triton.getSymbolicVariable(k), value) 85 print('[+] Symbolic variable %02d = %02x (%c)' %(k, value, chr(value))) 86 87 # Next 88 pc = Triton.getConcreteRegisterValue(Triton.registers.rip) 89 90 print('[+] Emulation done.') 91 return 92 93 94# Load segments into triton. 95def loadBinary(path): 96 import lief 97 binary = lief.parse(path) 98 phdrs = binary.segments 99 for phdr in phdrs: 100 size = phdr.physical_size 101 vaddr = phdr.virtual_address 102 print('[+] Loading 0x%06x - 0x%06x' %(vaddr, vaddr+size)) 103 Triton.setConcreteMemoryAreaValue(vaddr, phdr.content) 104 return 105 106 107if __name__ == '__main__': 108 # Define the target architecture 109 Triton.setArchitecture(ARCH.X86_64) 110 111 # Define symbolic optimizations 112 Triton.setMode(MODE.ALIGNED_MEMORY, True) 113 Triton.setMode(MODE.ONLY_ON_SYMBOLIZED, True) 114 115 # Load the binary 116 loadBinary(os.path.join(os.path.dirname(__file__), 'r100.bin')) 117 118 # Define a fake stack 119 Triton.setConcreteRegisterValue(Triton.registers.rbp, 0x7fffffff) 120 Triton.setConcreteRegisterValue(Triton.registers.rsp, 0x6fffffff) 121 122 # Define an user input 123 Triton.setConcreteRegisterValue(Triton.registers.rdi, 0x10000000) 124 125 # Symbolize user inputs (30 bytes) 126 for index in range(30): 127 Triton.symbolizeMemory(MemoryAccess(0x10000000+index, CPUSIZE.BYTE)) 128 129 # Emulate from the verification function 130 emulate(0x4006FD) 131 132 sys.exit(0) 133 134