Import claripy through the angr package

angrop/chain_builder/builder.py

@@ -8,7 +8,7 @@
 from collections import defaultdict
 
 import angr
-import claripy
+from angr import claripy
 
 from .. import rop_utils
 from ..errors import RopException
@@ -185,7 +185,7 @@ def _build_ast_constraints(self, ast):
             var_map[reg] = (old_var, new_var)
 
         #  if this ast is a tree, record all the children_asts
-        for x in ast.children_asts():
+        for x in rop_utils.children_asts(ast):
             if x.op != 'BVS':
                 continue
             name = x.args[0]
@@ -210,7 +210,7 @@ def _solve_ast_constraint(self, ast, value):
         if ast.op == 'BVS':
             variables.add(ast)
         else:
-            for x in ast.children_asts():
+            for x in rop_utils.children_asts(ast):
                 if x.op != 'BVS':
                     continue
                 variables.add(x)
@@ -252,7 +252,7 @@ def _rebalance_ast(self, lhs, rhs, mode='stack'):
         # in some cases, we can just solve it
         if mode == 'stack' and lhs.symbolic and not rhs.symbolic and len(lhs.variables) == 1 and lhs.depth > 1:
             target_ast = None
-            for ast in lhs.children_asts():
+            for ast in rop_utils.children_asts(lhs):
                 if ast.op == 'BVS' and ast.args[0].startswith('symbolic_stack'):
                     target_ast = ast
                     break

angrop/chain_builder/func_caller.py

@@ -2,7 +2,7 @@
 import logging
 
 import angr
-import claripy
+from angr import claripy
 from angr.calling_conventions import SimRegArg, SimStackArg
 
 from .builder import Builder

angrop/chain_builder/mem_writer.py

@@ -3,7 +3,7 @@
 from collections import defaultdict
 
 import angr
-import claripy
+from angr import claripy
 
 from .builder import Builder
 from .. import rop_utils
@@ -101,7 +101,7 @@ def concretize(self, addr_val, data):
             if not val.symbolic or not val.ast.variables:
                 continue
             if list(val.ast.variables)[0].startswith('addr_'):
-                test_ast = claripy.algorithm.replace(expr=val.ast,
+                test_ast = claripy.replace(expr=val.ast,
                                           old=self.addr_bv,
                                           new=addr_val.data)
                 new = addr_val.copy()
@@ -112,7 +112,7 @@ def concretize(self, addr_val, data):
                 continue
             if list(val.ast.variables)[0].startswith('data_'):
                 var = claripy.BVV(struct.unpack(fmt, data.ljust(arch_bytes, b'\x00'))[0], len(self.data_bv))
-                test_ast = claripy.algorithm.replace(expr=val.ast,
+                test_ast = claripy.replace(expr=val.ast,
                                           old=self.data_bv,
                                           new=var)
                 if len(test_ast) < arch_bits: # type: ignore

angrop/chain_builder/reg_setter.py

@@ -3,7 +3,7 @@
 from collections import defaultdict, Counter
 from functools import cmp_to_key
 
-import claripy
+from angr import claripy
 import networkx as nx
 from angr.errors import SimUnsatError
 
@@ -66,7 +66,7 @@ def bootstrap(self):
     def _effect_tuple(self, g):
         reg = list(g.concrete_reg_changes.keys())[0]
         init_ast, final_ast = g.concrete_reg_changes[reg]
-        val = claripy.algorithm.replace(expr=final_ast,
+        val = claripy.replace(expr=final_ast,
                                         old=init_ast,
                                         new=claripy.BVV(0, self.project.arch.bits))
         op = final_ast.op
@@ -707,7 +707,7 @@ def _find_add_chain(self, reg, val) -> list[RopGadget|RopBlock]:
         for g1 in concrete_setter_gadgets:
             for g2 in delta_gadgets:
                 init_ast, final_ast = g2.concrete_reg_changes[reg]
-                ast = claripy.algorithm.replace(expr=final_ast,
+                ast = claripy.replace(expr=final_ast,
                                                 old=init_ast,
                                                 new=claripy.BVV(g1.concrete_regs[reg], arch_bits))
                 if ast.concrete_value != val.concreted:

angrop/chain_builder/shifter.py

@@ -1,7 +1,7 @@
 import logging
 from collections import defaultdict
 
-import claripy
+from angr import claripy
 
 from .. import rop_utils
 from .builder import Builder

angrop/gadget_finder/gadget_analyzer.py

@@ -7,7 +7,7 @@
 
 import angr
 import pyvex
-import claripy
+from angr import claripy
 from angr.analyses.bindiff import differing_constants
 from angr.analyses.bindiff import UnmatchedStatementsException
 from angr.errors import SimEngineError, SimMemoryError
@@ -105,7 +105,7 @@ def filter_func(state):
             simgr.move(from_stash='active', to_stash='syscall',
                        filter_func=lambda s: rop_utils.is_in_kernel(self.project, s))
 
-        except (claripy.ClaripySolverInterruptError, claripy.errors.ClaripyZ3Error, ValueError): # type: ignore
+        except (claripy.ClaripySolverInterruptError, claripy.errors.ClaripyError, ValueError): # type: ignore
             return [], []
         except (claripy.ClaripyFrontendError,
                 angr.engines.vex.claripy.ccall.CCallMultivaluedException) as e: # type: ignore
@@ -170,7 +170,7 @@ def _analyze_gadget(self, addr, allow_conditional_branches):
             except RopException as e:
                 l.debug("... %s", e)
                 continue
-            except (claripy.ClaripySolverInterruptError, claripy.errors.ClaripyZ3Error, ValueError): # type: ignore
+            except (claripy.ClaripySolverInterruptError, claripy.errors.ClaripyError, ValueError): # type: ignore
                 continue
             except (claripy.ClaripyFrontendError,
                     angr.engines.vex.claripy.ccall.CCallMultivaluedException) as e: # type: ignore
@@ -621,7 +621,7 @@ def _check_reg_change_dependencies(self, init_state, final_state, gadget):
             final_reg = final_state.registers.load(reg)
             if init_reg is final_reg:
                 continue
-            ast = claripy.algorithm.replace(expr=final_reg, old=init_reg, new=claripy.BVV(0, arch_bits))
+            ast = claripy.replace(expr=final_reg, old=init_reg, new=claripy.BVV(0, arch_bits))
             if ast.symbolic:
                 continue
             gadget.concrete_reg_changes[reg] = (init_reg, final_reg)
@@ -1015,6 +1015,14 @@ def _build_mem_change(self, read_action, write_action, gadget, init_state, final
                 return None
         data_stack_controllers = {x for x in sym_data.variables if x.startswith('symbolic_stack')}
 
+        # a memory change whose delta has no controller is a pure constant change (e.g. `dec [rax]`).
+        # we only recognize such constant changes at full word granularity. sub-word constant changes
+        # (e.g. thumb `ldrh; subs; strh`) are not usable by the mem-change chain builder; historically
+        # they were filtered out incidentally because claripy left the store data wrapped in an
+        # Extract, but clarirs simplifies that away, so we reject them explicitly here.
+        if not data_controllers and not data_stack_controllers:
+            if write_action.data.ast.size() != self.project.arch.bits:
+                return None
 
         mem_change = self._build_mem_access(read_action, gadget, init_state, final_state)
         mem_change.op = write_action.data.ast.op

angrop/rop.py

@@ -1,3 +1,4 @@
+import os
 import pickle
 import inspect
 import logging
@@ -193,6 +194,7 @@ def save_gadgets(self, path):
         Saves gadgets in a file.
         :param path: A path for a file where the gadgets are stored
         """
+        os.makedirs(os.path.dirname(path) or ".", exist_ok=True)
         with open(path, "wb") as f:
             pickle.dump(self._get_cache_tuple(), f)
         for g in self._all_gadgets:

angrop/rop_chain.py

@@ -268,7 +268,14 @@ def __concretize_chain_values(self, constraints=None):
                 solver_state.solver.add(expr)
                 if not solver_state.solver.satisfiable():
                     raise RopException("bad chain!")
-            concrete_vals.append((solver_state.solver.eval(ast), value.rebase))
+            concrete = solver_state.solver.eval(ast)
+            # pin the concretized value so that values sharing constraints with this
+            # one (e.g. two registers tied by `r12 + rbx*8 == ptr`) are concretized
+            # consistently. without this, each eval() may pick a different satisfying
+            # model and the concrete values won't jointly satisfy the constraints.
+            if ast.symbolic:
+                solver_state.solver.add(ast == concrete)
+            concrete_vals.append((concrete, value.rebase))
 
         return concrete_vals
 

angrop/rop_utils.py

@@ -5,12 +5,31 @@
 import threading
 
 import angr
-import claripy
+from angr import claripy
 from angr.engines.successors import SimSuccessors
 
 from .errors import RegNotFoundException, RopException, RopTimeoutException
 from .rop_value import RopValue
 
+
+def children_asts(ast):
+    """
+    Iterate over the nested children ASTs of ``ast`` (depth-first).
+
+    Replaces claripy's ``Base.children_asts()``, which clarirs does not
+    provide; clarirs ASTs only expose their immediate ``.args``.
+    """
+    queue = [iter(ast.args)]
+    while queue:
+        try:
+            child = next(queue[-1])
+        except StopIteration:
+            queue.pop()
+            continue
+        if isinstance(child, claripy.ast.Base):
+            queue.append(iter(child.args))
+            yield child
+
 def addr_to_asmstring(project, addr):
     block = project.factory.block(addr)
     return "; ".join(["%s %s" %(i.mnemonic, i.op_str) for i in block.capstone.insns])
@@ -83,7 +102,7 @@ def get_ast_controllers(state, ast, reg_deps) -> set:
             if not state.registers.load(r).symbolic:
                 continue
             reg_sym_val = state.registers.load(r)
-            test_ast = claripy.algorithm.replace(expr=test_ast,
+            test_ast = claripy.replace(expr=test_ast,
                                       old=reg_sym_val,
                                       new=claripy.BVV(test_val, reg_sym_val.size()))
         # we consider 32-bit control on 64-bit system valid
@@ -111,7 +130,7 @@ def get_ast_const_offset(state, ast, reg_deps) -> int:
     # This is faster than eval with extra contraints
     for reg in reg_deps:
         reg_val = state.registers.load(reg)
-        ast = claripy.algorithm.replace(
+        ast = claripy.replace(
             expr=ast, old=reg_val, new=zero_val)
 
     assert not ast.symbolic
@@ -178,7 +197,7 @@ def fast_unconstrained_check(state, ast):
 
     passes_prefilter = True
 
-    for a in ast.children_asts():
+    for a in children_asts(ast):
         if a.op not in good_ops:
             passes_prefilter = False
         # check for x __add__ x which is constrained
@@ -255,7 +274,7 @@ def get_reg_name(arch, reg_offset):
 def bits_extended(ast):
     if ast.op in ('ZeroExt', 'SignExt'):
         return ast.args[0]
-    for c in ast.children_asts():
+    for c in children_asts(ast):
         if c.op in ('ZeroExt', 'SignExt'):
             return c.args[0]
     return None
@@ -296,10 +315,14 @@ def make_initial_state(project, stack_gsize):
     initial_state.options.discard(angr.options.CGC_ZERO_FILL_UNCONSTRAINED_MEMORY)
     initial_state.options.update({angr.options.TRACK_REGISTER_ACTIONS, angr.options.TRACK_MEMORY_ACTIONS,
                                   angr.options.TRACK_JMP_ACTIONS, angr.options.TRACK_CONSTRAINT_ACTIONS})
-    symbolic_stack = claripy.Concat(*[
-        initial_state.solver.BVS(f"symbolic_stack_{i}", project.arch.bits) for i in range(stack_gsize)
-    ])
-    initial_state.memory.store(initial_state.regs.sp, symbolic_stack)
+    # stack_gsize may be 0 (a gadget that controls no stack); skip the store in
+    # that case. claripy tolerated claripy.Concat() with no arguments, but
+    # clarirs rejects an empty operand list.
+    if stack_gsize > 0:
+        symbolic_stack = claripy.Concat(*[
+            initial_state.solver.BVS(f"symbolic_stack_{i}", project.arch.bits) for i in range(stack_gsize)
+        ])
+        initial_state.memory.store(initial_state.regs.sp, symbolic_stack)
     if initial_state.arch.bp_offset != initial_state.arch.sp_offset:
         initial_state.regs.bp = initial_state.regs.sp + 20*initial_state.arch.bytes
     initial_state.solver._solver.timeout = 1000  # only solve for a second at most

angrop/rop_value.py

@@ -1,4 +1,4 @@
-import claripy
+from angr import claripy
 
 class RopValue:
     """

tests/test_badbytes.py

@@ -36,7 +36,7 @@ def test_badbyte():
     if os.path.exists(cache_path):
         rop.load_gadgets(cache_path)
     else:
-        rop.find_gadgets()
+        rop.find_gadgets_single_threaded()
         rop.save_gadgets(cache_path)
 
     # make sure it can set 0 first
@@ -91,7 +91,7 @@ def test_badbyte_transform():
     if os.path.exists(cache_path):
         rop.load_gadgets(cache_path)
     else:
-        rop.find_gadgets()
+        rop.find_gadgets_single_threaded()
         rop.save_gadgets(cache_path)
 
     rop.set_badbytes([0x00, 0x0A])
@@ -111,7 +111,7 @@ def test_badbyte_multibyte():
     if os.path.exists(cache_path):
         rop.load_gadgets(cache_path)
     else:
-        rop.find_gadgets()
+        rop.find_gadgets_single_threaded()
         rop.save_gadgets(cache_path)
 
     rop.set_badbytes([0x00, 0x0A])
@@ -133,7 +133,7 @@ def test_hard_regs_loop():
     if os.path.exists(cache_path):
         rop.load_gadgets(cache_path)
     else:
-        rop.find_gadgets()
+        rop.find_gadgets_single_threaded()
         rop.save_gadgets(cache_path)
 
     rop.set_badbytes([0x00, 0x0A])