Bumped version number to 1.5.2. Pinned dependencies so that they must…

… be exactly equal to specific versions. Updated cozy to work with claripy 9.2.130. Fixed paths for mrzr test scripts.

cozy/concolic/exploration.py

@@ -84,15 +84,15 @@ 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:
             raise RuntimeError("Some symbols were unconstrained when checking for truthiness after substitution. Are you sure that all symbols are present in the set you passed to generate_concrete? Another likely cause of this error is a hook introducing a fresh symbolic variable")
 
     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]]):
         """

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:

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
+            # 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

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,22 +63,22 @@ 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)
                 and self.state.solver.eval(a_len) == self.state.solver.eval(b_len) == 0
             ):
                 # 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,39 +123,39 @@ 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,
                                 a_byte <= ord("z"),
                                 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

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)

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)