diff --git a/cozy/concolic/exploration.py b/cozy/concolic/exploration.py index d08c7d2..59b6e10 100644 --- a/cozy/concolic/exploration.py +++ b/cozy/concolic/exploration.py @@ -84,7 +84,7 @@ def is_satisfied(self, constraints: list[claripy.ast.bool]) -> bool: :rtype: bool :return: If the constraints are True after substitution, then True is returned. Otherwise returns False. """ - expr = claripy.And(*constraints).replace_dict(self._replacement_dict) + expr = claripy.replace_dict(claripy.And(*constraints), self._replacement_dict) if len(expr.variables) == 0: return expr.is_true() else: @@ -92,7 +92,7 @@ def is_satisfied(self, constraints: list[claripy.ast.bool]) -> bool: def _set_replacement_dict(self, concrete): self.concrete = concrete - self._replacement_dict = {sym.cache_key: val for (sym, val) in concrete.items()} + self._replacement_dict = {sym.hash(): val for (sym, val) in concrete.items()} def set_concrete(self, simgr, concrete: dict[typing.Union[claripy.BVS, claripy.FPS], typing.Union[claripy.BVV, claripy.FPV]]): """ diff --git a/cozy/concrete.py b/cozy/concrete.py index 72f9f9c..ed3adb9 100644 --- a/cozy/concrete.py +++ b/cozy/concrete.py @@ -15,16 +15,19 @@ def traverse(elem, bundle_symbols): preorder_fold(elem.body, traverse, bundle_symbols) return bundle_symbols + # First, walk over the state bundle to find all symbols contained within the nested data structure extra_symbols = preorder_fold(state_bundle, traverse, set()) + # Generate up to n models, finding the substitutions for all the symbols + # Each model maps each symbol found in the previous step to a concrete value models = claripy_ext.model(solver.constraints, extra_symbols=extra_symbols, n=n) ret = [] for model in models: - replacement_dict = {sym.cache_key: val for (sym, val) in model.items()} + replacement_dict = {sym.hash(): val for (sym, val) in model.items()} def f(elem): if isinstance(elem, claripy.ast.Base): - return elem.replace_dict(replacement_dict) + return claripy.replace_dict(elem, replacement_dict) elif isinstance(elem, PerformedSideEffect): return ConcretePerformedSideEffect(elem, elem.state_history, fmap(elem.body, f), concrete_post_processor=elem.concrete_post_processor, label=elem.label) else: diff --git a/cozy/hooks/strlen.py b/cozy/hooks/strlen.py index 640a242..7375ca7 100644 --- a/cozy/hooks/strlen.py +++ b/cozy/hooks/strlen.py @@ -1,4 +1,7 @@ +from functools import reduce + import angr +import claripy from angr.sim_options import MEMORY_CHUNK_INDIVIDUAL_READS from angr.storage.memory_mixins.regioned_memory.abstract_address_descriptor import AbstractAddressDescriptor @@ -13,10 +16,10 @@ class strlen(angr.SimProcedure): def run(self, s, wchar=False, maxlen=None): if wchar: - null_seq = self.state.solver.BVV(0, 16) + null_seq = claripy.BVV(0, 16) char_size = 2 else: - null_seq = self.state.solver.BVV(0, 8) + null_seq = claripy.BVV(0, 8) char_size = 1 max_symbolic_bytes = self.state.libc.buf_symbolic_bytes @@ -35,7 +38,7 @@ def run(self, s, wchar=False, maxlen=None): addr_desc: AbstractAddressDescriptor = self.state.memory._normalize_address(s) # size_t - length = self.state.solver.ESI(self.arch.bits) + lengths = [] for s_aw in self.state.memory._concretize_address_descriptor(addr_desc, None): s_ptr = s_aw.to_valueset(self.state) r, c, i = self.state.memory.find( @@ -47,55 +50,62 @@ def run(self, s, wchar=False, maxlen=None): char_size=char_size, ) - self.max_null_index = max([self.max_null_index] + i) + self.max_null_index = max([self.max_null_index, *i]) # Convert r to the same region as s r_desc = self.state.memory._normalize_address(r) r_aw_iter = self.state.memory._concretize_address_descriptor( - r_desc, None, target_region=next(iter(s_ptr._model_vsa.regions.keys())) + r_desc, + None, + target_region=next( + iter(s_ptr.get_annotations_by_type(claripy.annotation.RegionAnnotation)) + ).region_id, ) for r_aw in r_aw_iter: r_ptr = r_aw.to_valueset(self.state) - length = length.union(r_ptr - s_ptr) - - return length - - else: - search_len = max_str_len + lengths.append(r_ptr - s_ptr) + + match len(lengths): + case 0: + return claripy.BVS("unnamed", self.state.arch.bits) + case 1: + return lengths[0] + case _: + return reduce(claripy.union, lengths) + + search_len = max_str_len + r, c, i = self.state.memory.find( + s, + null_seq, + search_len, + max_symbolic_bytes=max_symbolic_bytes, + chunk_size=chunk_size, + char_size=char_size, + ) + + # try doubling the search len and searching again + s_new = s + while c and all(con.is_false() for con in c): + s_new += search_len + search_len *= 2 r, c, i = self.state.memory.find( - s, + s_new, null_seq, search_len, max_symbolic_bytes=max_symbolic_bytes, chunk_size=chunk_size, char_size=char_size, ) - - # try doubling the search len and searching again - s_new = s - while c and all(con.is_false() for con in c): - s_new += search_len - search_len *= 2 - r, c, i = self.state.memory.find( - s_new, - null_seq, - search_len, - max_symbolic_bytes=max_symbolic_bytes, - chunk_size=chunk_size, - char_size=char_size, - ) - # stop searching after some reasonable limit - if search_len > 0x10000: - raise angr.SimMemoryLimitError("strlen hit limit of 0x10000") - - self.max_null_index = max(i) - self.state.add_constraints(*c) - result = r - s - - #if result.depth > 3: - # rresult = self.state.solver.BVS("strlen", len(result), key=("api", "strlen")) - # self.state.add_constraints(result == rresult) - # result = rresult - - return result \ No newline at end of file + # stop searching after some reasonable limit + if search_len > 0x10000: + raise angr.SimMemoryLimitError("strlen hit limit of 0x10000") + + self.max_null_index = max(i) + self.state.add_constraints(*c) + result = r - s + #if result.depth > 3: + # rresult = self.state.solver.BVS("strlen", len(result), key=("api", "strlen")) + # self.state.add_constraints(result == rresult) + # result = rresult + return result \ No newline at end of file diff --git a/cozy/hooks/strncmp.py b/cozy/hooks/strncmp.py index 468a7e8..1844d9f 100644 --- a/cozy/hooks/strncmp.py +++ b/cozy/hooks/strncmp.py @@ -1,4 +1,5 @@ import angr +import claripy import logging @@ -50,9 +51,9 @@ def run( maxlen = max(a_strlen.max_null_index, b_strlen.max_null_index) match_constraints.append( - self.state.solver.Or( + claripy.Or( a_len == b_len, - self.state.solver.And(self.state.solver.UGE(a_len, limit), self.state.solver.UGE(b_len, limit)), + claripy.And(claripy.UGE(a_len, limit), claripy.UGE(b_len, limit)), ) ) @@ -62,7 +63,7 @@ def run( if self.state.solver.single_valued(limit) and self.state.solver.eval(limit) == 0: # limit is 0 l.debug("returning equal for 0-limit") - return self.state.solver.BVV(0, 32) + return claripy.BVV(0, 32) elif ( self.state.solver.single_valued(a_len) and self.state.solver.single_valued(b_len) @@ -70,14 +71,14 @@ def run( ): # two empty strings l.debug("returning equal for two empty strings") - return self.state.solver.BVV(0, 32) + return claripy.BVV(0, 32) else: # all other cases fall into this branch l.debug("returning non-equal for comparison of an empty string and a non-empty string") if a_strlen.max_null_index == 0: - return self.state.solver.BVV(-1, 32) + return claripy.BVV(-1, 32) else: - return self.state.solver.BVV(1, 32) + return claripy.BVV(1, 32) # the bytes max_byte_len = maxlen * char_size @@ -111,9 +112,9 @@ def run( if a_conc != b_conc: l.debug("... found mis-matching concrete bytes 0x%x and 0x%x", a_conc, b_conc) if a_conc < b_conc: - return self.state.solver.BVV(-1, 32) + return claripy.BVV(-1, 32) else: - return self.state.solver.BVV(1, 32) + return claripy.BVV(1, 32) else: if self.state.mode == "static": return_values.append(a_byte - b_byte) @@ -122,17 +123,17 @@ def run( if self.state.mode != "static": if ignore_case: - byte_constraint = self.state.solver.Or( - self.state.solver.Or( + byte_constraint = claripy.Or( + claripy.Or( a_byte == b_byte, - self.state.solver.And( + claripy.And( ord("A") <= a_byte, a_byte <= ord("Z"), ord("a") <= b_byte, b_byte <= ord("z"), b_byte - ord(" ") == a_byte, ), - self.state.solver.And( + claripy.And( ord("A") <= b_byte, b_byte <= ord("Z"), ord("a") <= a_byte, @@ -140,21 +141,21 @@ def run( a_byte - ord(" ") == b_byte, ), ), - self.state.solver.ULT(a_len, i), - self.state.solver.ULE(limit, i), + claripy.ULT(a_len, i), + claripy.ULE(limit, i), ) else: - byte_constraint = self.state.solver.Or( - a_byte == b_byte, self.state.solver.ULT(a_len, i), self.state.solver.ULE(limit, i) + byte_constraint = claripy.Or( + a_byte == b_byte, claripy.ULT(a_len, i), claripy.ULE(limit, i) ) match_constraints.append(byte_constraint) if concrete_run: l.debug("concrete run made it to the end!") - return self.state.solver.BVV(0, 32) + return claripy.BVV(0, 32) if self.state.mode == "static": - ret_expr = self.state.solver.ESI(8) + ret_expr = claripy.ESI(8) for expr in return_values: ret_expr = ret_expr.union(expr) @@ -164,28 +165,28 @@ def run( # make the constraints l.debug("returning symbolic") - match_constraint = self.state.solver.And(*match_constraints) - nomatch_constraint = self.state.solver.Not(match_constraint) + match_constraint = claripy.And(*match_constraints) + nomatch_constraint = claripy.Not(match_constraint) # l.debug("match constraints: %s", match_constraint) # l.debug("nomatch constraints: %s", nomatch_constraint) - match_case = self.state.solver.And(limit != 0, match_constraint) + match_case = claripy.And(limit != 0, match_constraint) l0_case = limit == 0 - empty_case = self.state.solver.And(a_strlen.ret_expr == 0, b_strlen.ret_expr == 0) + empty_case = claripy.And(a_strlen.ret_expr == 0, b_strlen.ret_expr == 0) - zero_case = self.state.solver.Or(match_case, l0_case, empty_case) + zero_case = claripy.Or(match_case, l0_case, empty_case) - #nomatch_case = self.state.solver.And(limit != 0, nomatch_constraint) + #nomatch_case = claripy.And(limit != 0, nomatch_constraint) #one_case = nomatch_case - ret_expr = self.state.solver.If(zero_case, self.state.solver.BVV(0, 32), self.state.solver.BVV(1, 32)) + ret_expr = claripy.If(zero_case, claripy.BVV(0, 32), claripy.BVV(1, 32)) - #match_case = self.state.solver.And(limit != 0, match_constraint, ret_expr == 0) - #nomatch_case = self.state.solver.And(limit != 0, nomatch_constraint, ret_expr == 1) - #l0_case = self.state.solver.And(limit == 0, ret_expr == 0) - #empty_case = self.state.solver.And(a_strlen.ret_expr == 0, b_strlen.ret_expr == 0, ret_expr == 0) + #match_case = claripy.And(limit != 0, match_constraint, ret_expr == 0) + #nomatch_case = claripy.And(limit != 0, nomatch_constraint, ret_expr == 1) + #l0_case = claripy.And(limit == 0, ret_expr == 0) + #empty_case = claripy.And(a_strlen.ret_expr == 0, b_strlen.ret_expr == 0, ret_expr == 0) - #self.state.add_constraints(self.state.solver.Or(match_case, nomatch_case, l0_case, empty_case)) + #self.state.add_constraints(claripy.Or(match_case, nomatch_case, l0_case, empty_case)) return ret_expr diff --git a/cozy/hooks/strtok_r.py b/cozy/hooks/strtok_r.py index 4efa812..94f84a4 100644 --- a/cozy/hooks/strtok_r.py +++ b/cozy/hooks/strtok_r.py @@ -1,5 +1,5 @@ import angr - +import claripy import logging l = logging.getLogger(name=__name__) @@ -12,10 +12,10 @@ def run(self, str_ptr, delim_ptr, save_ptr, str_strlen=None, delim_strlen=None): if self.state.libc.simple_strtok: malloc = angr.SIM_PROCEDURES["libc"]["malloc"] token_ptr = self.inline_call(malloc, self.state.libc.strtok_token_size).ret_expr - r = self.state.solver.If( + r = claripy.If( self.state.solver.Unconstrained("strtok_case", self.state.arch.bits) == 0, token_ptr, - self.state.solver.BVV(0, self.state.arch.bits), + claripy.BVV(0, self.state.arch.bits), ) self.state.libc.strtok_heap.append(token_ptr) return r @@ -29,7 +29,7 @@ def run(self, str_ptr, delim_ptr, save_ptr, str_strlen=None, delim_strlen=None): saved_str_ptr = self.state.memory.load( save_ptr, self.state.arch.bytes, endness=self.state.arch.memory_endness ) - start_ptr = self.state.solver.If(str_ptr == 0, saved_str_ptr, str_ptr) + start_ptr = claripy.If(str_ptr == 0, saved_str_ptr, str_ptr) l.debug("... getting the lengths") str_strlen = self.inline_call(strlen, start_ptr) if str_strlen is None else str_strlen @@ -40,8 +40,8 @@ def run(self, str_ptr, delim_ptr, save_ptr, str_strlen=None, delim_strlen=None): where = self.inline_call( strstr, start_ptr, delim_ptr, haystack_strlen=str_strlen, needle_strlen=delim_strlen ) - write_length = self.state.solver.If(where.ret_expr != 0, delim_strlen.ret_expr, 0) - write_content = self.state.solver.BVV(0, delim_strlen.max_null_index * 8) + write_length = claripy.If(where.ret_expr != 0, delim_strlen.ret_expr, 0) + write_content = claripy.BVV(0, delim_strlen.max_null_index * 8) # do a symbolic write (we increment the limit because of the possibility that the write target is 0, # in which case the length will be 0, anyways) @@ -56,7 +56,7 @@ def run(self, str_ptr, delim_ptr, save_ptr, str_strlen=None, delim_strlen=None): l.debug("... creating the return address") new_start = write_length + where.ret_expr - new_state = self.state.solver.If(new_start != 0, new_start, start_ptr) + new_state = claripy.If(new_start != 0, new_start, start_ptr) l.debug("... saving the state") self.state.memory.store(save_ptr, new_state, endness=self.state.arch.memory_endness) diff --git a/cozy/server.py b/cozy/server.py index 7856c33..b523fb1 100644 --- a/cozy/server.py +++ b/cozy/server.py @@ -53,7 +53,9 @@ def start_viz_server(pre={}, post={}, open_browser=False, port=8080): thread.daemon = True thread.start() if open_browser: - webbrowser.open_new("localhost:" + str(port) + "/?pre=/pre&post=/post") + url = "http://localhost:" + str(port) + "/?pre=/pre&post=/post" + print(f"Open the browser and navigate to {url} if the browser doesn't open now") + webbrowser.open_new(url) while True: time.sleep(1) diff --git a/examples/mrzr_tob_no_fail_check.py b/examples/mrzr_tob_no_fail_check.py index ce8ce4b..89552f4 100644 --- a/examples/mrzr_tob_no_fail_check.py +++ b/examples/mrzr_tob_no_fail_check.py @@ -11,10 +11,10 @@ onMessageLength_prototype = "void f(void *this, void *conn, void **buffer, unsigned int size, unsigned char success)" -proj_prepatched = cozy.project.Project(f"{amp_hackathon_path}/bin/libroscpp.so") +proj_prepatched = cozy.project.Project("test_programs/amp_target3_hackathon/libroscpp.so") proj_prepatched.add_prototype(onMessageLength_mangled, onMessageLength_prototype) -proj_postpatched = cozy.project.Project(f"{amp_hackathon_path}/operator_patches/classroom_MRZR_sysinfo/repro_goodandbad_patches/withoutfailcheck.bin") +proj_postpatched = cozy.project.Project("test_programs/amp_target3_hackathon/libroscpp_tob_no_fail_check.so") proj_postpatched.add_prototype(onMessageLength_mangled, onMessageLength_prototype) # size is a symbolic variable that ends up being passed to the onMessageLength function. This symbolic variable @@ -157,6 +157,8 @@ def bp(state): print("\nComparison Results, pre-patch vs post-patch:\n") print(comparison_results.report(args)) +cozy.execution_graph.visualize_comparison(proj_prepatched, proj_postpatched, pre_patched_results, post_patched_results, comparison_results, open_browser=True, args=args, num_examples=2) + cozy.execution_graph.dump_comparison(proj_prepatched, proj_postpatched, pre_patched_results, post_patched_results, comparison_results, diff --git a/examples/mrzr_with_fail_check.py b/examples/mrzr_with_fail_check.py index 22586a5..575eb03 100644 --- a/examples/mrzr_with_fail_check.py +++ b/examples/mrzr_with_fail_check.py @@ -187,6 +187,9 @@ def bp(state): comparison_results = cozy.analysis.Comparison(pre_patched_results, tob_patched_results) print("\nComparison Results, pre-patch vs post-patch:\n") print(comparison_results.report(args)) + +cozy.execution_graph.visualize_comparison(proj_prepatched, proj_postpatched, pre_patched_results, tob_patched_results, comparison_results) + cozy.execution_graph.dump_comparison(proj_prepatched, proj_tob_patch, pre_patched_results, tob_patched_results, comparison_results, diff --git a/pyproject.toml b/pyproject.toml index 37e9146..5117cf2 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "cozy-re" -version = "1.5.1" +version = "1.5.2" authors = [ { name="Caleb Helbling", email="chelbling@draper.com" }, { name="Graham Leach-Krouse", email="gleach-krouse@draper.com"}, @@ -18,11 +18,11 @@ classifiers = [ "Operating System :: OS Independent", ] dependencies = [ - "angr >= 9.2.96", - "networkx >= 3.0", - "claripy >= 9.2.96", - "portion >= 2.4.1", - "textual >= 0.60.1", + "angr == 9.2.130", + "networkx == 3.3", + "claripy == 9.2.130", + "portion == 2.4.2", + "textual == 0.71.0", ] [project.urls] diff --git a/setup.py b/setup.py index 666dc26..55afea2 100644 --- a/setup.py +++ b/setup.py @@ -5,7 +5,7 @@ setup( name='cozy-re', - version='1.5.1', + version='1.5.2', description='Python tool for comparing binaries via symbolic execution utilizing the angr framework.', long_description=long_description, author='Caleb Helbling',