|
| 1 | +import angr |
| 2 | + |
| 3 | +import cozy |
| 4 | +import cozy.concolic |
| 5 | +import claripy |
| 6 | + |
| 7 | +proj_prepatched = cozy.project.Project('test_programs/injection_demo/injectionAttack') |
| 8 | +proj_postpatched_good = cozy.project.Project('test_programs/injection_demo/injectionAttack-goodPatch-patcherex') |
| 9 | +# proj_postpatched_bad = cozy.project.Project('test_programs/injection_demo/injectionAttack-badPatch-patcherex') |
| 10 | +# ↑ uses too much memory for CI... |
| 11 | + |
| 12 | +proj_prepatched.add_prototype("main", "int main(int argc, char **argv)") |
| 13 | +proj_postpatched_good.add_prototype("main", "int main(int argc, char **argv)") |
| 14 | +# proj_postpatched_bad.add_prototype("main", "int main(int argc, char **argv)") |
| 15 | + |
| 16 | +INPUT_LEN = 20 |
| 17 | + |
| 18 | +command_symbols = [claripy.BVS('command', 8) for _ in range(INPUT_LEN - 1)] |
| 19 | +role_symbols = [claripy.BVS('role', 8) for _ in range(INPUT_LEN - 1)] |
| 20 | +data_symbols = [claripy.BVS('data', 8) for _ in range(INPUT_LEN - 1)] |
| 21 | + |
| 22 | +symbols = set() |
| 23 | +symbols.update(command_symbols) |
| 24 | +symbols.update(role_symbols) |
| 25 | +symbols.update(data_symbols) |
| 26 | + |
| 27 | +command_symbols.append(claripy.BVV(0, 8)) |
| 28 | +role_symbols.append(claripy.BVV(0, 8)) |
| 29 | +data_symbols.append(claripy.BVV(0, 8)) |
| 30 | + |
| 31 | +# This function ensures that once a null terminating byte is seen, all subsequent bytes in the string |
| 32 | +# must be null (\0) bytes |
| 33 | +def add_str_constraints(sess: cozy.project.Session): |
| 34 | + def constrain_lst(lst): |
| 35 | + for i in range(len(lst) - 2): |
| 36 | + sym_a = lst[i] |
| 37 | + sym_b = lst[i + 1] |
| 38 | + # Constrain the subsequent byte only if the first byte is \0 |
| 39 | + sess.add_constraints(sym_b == claripy.If(sym_a == 0, 0, sym_b)) |
| 40 | + constrain_lst(command_symbols) |
| 41 | + constrain_lst(role_symbols) |
| 42 | + constrain_lst(data_symbols) |
| 43 | + |
| 44 | +class sprintf(angr.SimProcedure): |
| 45 | + # pylint: disable=arguments-differ |
| 46 | + def run(self, dst, format_str): |
| 47 | + strlen = angr.SIM_PROCEDURES["libc"]["strlen"] |
| 48 | + strncpy = angr.SIM_PROCEDURES["libc"]["strncpy"] |
| 49 | + |
| 50 | + command = self.va_arg("char *") |
| 51 | + role = self.va_arg("char *") |
| 52 | + data = self.va_arg("char *") |
| 53 | + |
| 54 | + command_len = self.inline_call(strlen, command).ret_expr |
| 55 | + role_len = self.inline_call(strlen, role).ret_expr |
| 56 | + data_len = self.inline_call(strlen, data).ret_expr |
| 57 | + |
| 58 | + addr = dst |
| 59 | + |
| 60 | + self.state.mem[addr].char = ord('c') |
| 61 | + addr = addr + 1 |
| 62 | + self.state.mem[addr].char = ord(':') |
| 63 | + addr = addr + 1 |
| 64 | + |
| 65 | + self.inline_call(strncpy, addr, command, command_len + 1, src_len=command_len) |
| 66 | + addr = addr + command_len |
| 67 | + |
| 68 | + self.state.mem[addr].char = ord(';') |
| 69 | + addr = addr + 1 |
| 70 | + self.state.mem[addr].char = ord('r') |
| 71 | + addr = addr + 1 |
| 72 | + self.state.mem[addr].char = ord(':') |
| 73 | + addr = addr + 1 |
| 74 | + |
| 75 | + self.inline_call(strncpy, addr, role, role_len + 1, src_len=role_len) |
| 76 | + addr = addr + role_len |
| 77 | + |
| 78 | + self.state.mem[addr].char = ord(';') |
| 79 | + addr = addr + 1 |
| 80 | + self.state.mem[addr].char = ord('d') |
| 81 | + addr = addr + 1 |
| 82 | + self.state.mem[addr].char = ord(':') |
| 83 | + addr = addr + 1 |
| 84 | + |
| 85 | + self.inline_call(strncpy, addr, data, data_len + 1, src_len=data_len) |
| 86 | + |
| 87 | + return command_len + role_len + data_len + 8 |
| 88 | + |
| 89 | +def setup(proj: cozy.project.Project): |
| 90 | + proj.hook_symbol('sprintf', sprintf, replace=True) |
| 91 | + proj.hook_symbol('strlen', cozy.hooks.strlen.strlen, replace=True) |
| 92 | + proj.hook_symbol('strncmp', cozy.hooks.strncmp.strncmp, replace=True) |
| 93 | + proj.hook_symbol('strtok_r', cozy.hooks.strtok_r.strtok_r, replace=True) |
| 94 | + |
| 95 | + sess = proj.session("main") |
| 96 | + |
| 97 | + root_cond = ((role_symbols[0] == ord('r')) & |
| 98 | + (role_symbols[1] == ord('o')) & |
| 99 | + (role_symbols[2] == ord('o')) & |
| 100 | + (role_symbols[3] == ord('t')) & |
| 101 | + (role_symbols[4] == 0)) |
| 102 | + guest_cond = ((role_symbols[0] == ord('g')) & |
| 103 | + (role_symbols[1] == ord('u')) & |
| 104 | + (role_symbols[2] == ord('e')) & |
| 105 | + (role_symbols[3] == ord('s')) & |
| 106 | + (role_symbols[4] == ord('t')) & |
| 107 | + (role_symbols[5] == 0)) |
| 108 | + |
| 109 | + sess.add_constraints(root_cond | guest_cond) |
| 110 | + |
| 111 | + sess.state.libc.simple_strtok = False |
| 112 | + sess.state.libc.max_symbolic_strstr = 60 |
| 113 | + |
| 114 | + command = sess.malloc(20, name="command") |
| 115 | + role = sess.malloc(20, name="role") |
| 116 | + data = sess.malloc(20, name="data") |
| 117 | + |
| 118 | + for (i, sym) in enumerate(command_symbols): |
| 119 | + sess.mem[command + i].char = sym |
| 120 | + |
| 121 | + for (i, sym) in enumerate(role_symbols): |
| 122 | + sess.mem[role + i].char = sym |
| 123 | + |
| 124 | + for (i, sym) in enumerate(data_symbols): |
| 125 | + sess.mem[data + i].char = sym |
| 126 | + |
| 127 | + ptr_size_bits = sess.proj.arch.bits |
| 128 | + ptr_size_bytes = ptr_size_bits // 8 |
| 129 | + |
| 130 | + str_array = sess.malloc(4 * ptr_size_bits) |
| 131 | + |
| 132 | + endness = sess.proj.arch.memory_endness |
| 133 | + |
| 134 | + sess.store(str_array, claripy.BVV(0, ptr_size_bits)) |
| 135 | + sess.store(str_array + ptr_size_bytes, claripy.BVV(command, ptr_size_bits), endness=endness) |
| 136 | + sess.store(str_array + 2 * ptr_size_bytes, claripy.BVV(role, ptr_size_bits), endness=endness) |
| 137 | + sess.store(str_array + 3 * ptr_size_bytes, claripy.BVV(data, ptr_size_bits), endness=endness) |
| 138 | + |
| 139 | + argc = 4 |
| 140 | + argv = str_array |
| 141 | + args = [argc, argv] |
| 142 | + |
| 143 | + add_str_constraints(sess) |
| 144 | + |
| 145 | + def assertion_condition(state): |
| 146 | + # Assert that at this point in the program, the role the user originally inputted must be "root\0" |
| 147 | + return ((role_symbols[0] == ord('r')) & |
| 148 | + (role_symbols[1] == ord('o')) & |
| 149 | + (role_symbols[2] == ord('o')) & |
| 150 | + (role_symbols[3] == ord('t')) & |
| 151 | + (role_symbols[4] == 0)) |
| 152 | + |
| 153 | + directive = cozy.directive.Assert.from_fun_offset(proj, "delete", 0x0, assertion_condition, "Role is root at delete") |
| 154 | + sess.add_directives(directive) |
| 155 | + |
| 156 | + return (args, sess) |
| 157 | + |
| 158 | +(args_prepatched, prepatched_sess) = setup(proj_prepatched) |
| 159 | +# (args_postpatched_bad, postpatched_sess_bad) = setup(proj_postpatched_bad) |
| 160 | +(args_postpatched_good, postpatched_sess_good) = setup(proj_postpatched_good) |
| 161 | + |
| 162 | +prepatched_results = prepatched_sess.run(args_prepatched) |
| 163 | +# postpatched_results_bad = postpatched_sess_bad.run(args_postpatched_bad) |
| 164 | +postpatched_results_good = postpatched_sess_good.run(args_postpatched_good) |
| 165 | + |
| 166 | +def concrete_post_processor(args): |
| 167 | + def transform_str(characters): |
| 168 | + return [chr(n.concrete_value) if (n.concrete_value >= 32 and n.concrete_value <= 126) else n.concrete_value for n in characters] |
| 169 | + return [transform_str(cs) for cs in args] |
| 170 | + |
| 171 | +# comparison_bad = cozy.analysis.Comparison(prepatched_results, postpatched_results_bad, use_unsat_core=False) |
| 172 | +comparison_good = cozy.analysis.Comparison(prepatched_results, postpatched_results_good, use_unsat_core=False) |
| 173 | + |
| 174 | +# cozy.execution_graph.dump_comparison(proj_prepatched, proj_postpatched, |
| 175 | +# prepatched_results, postpatched_results, |
| 176 | +# comparison_bad, first_prog, second_prog, |
| 177 | +# output_file="cmp_injection_demo_bad.json", |
| 178 | +# concrete_post_processor=concrete_post_processor, |
| 179 | +# args=[command_symbols, role_symbols, data_symbols], |
| 180 | +# num_examples=2) |
| 181 | + |
| 182 | +cozy.execution_graph.dump_comparison(proj_prepatched, proj_postpatched, |
| 183 | + prepatched_results, postpatched_results, |
| 184 | + comparison_good, first_prog, second_prog, |
| 185 | + output_file="cmp_injection_demo_good.json", |
| 186 | + concrete_post_processor=concrete_post_processor, |
| 187 | + args=[command_symbols, role_symbols, data_symbols], |
| 188 | + num_examples=2) |
0 commit comments