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