SimUnsatError during gadget chain construction

[zardus]

This raises a SimUnsatError:

import angr
import angrop

p = angr.Project('/lib/x86_64-linux-gnu/libc.so.6')
r = p.analyses.ROP()
r.find_gadgets()
r.execve("/bin/bash")

....
ROP: 100% ||||||||||||||||||||||||||||||||||||||||||| Time: 1:09:08  52.15  B/s

In [5]: r.execve("/bin/bash")
WARNING | 2017-11-14 16:42:07,628 | angrop.chain_builder | writing to 0x7c8fc0
---------------------------------------------------------------------------
SimUnsatError                             Traceback (most recent call last)
<ipython-input-5-8326e2731458> in <module>()
----> 1 r.execve("/bin/bash")

/home/yans/code/angr/angrop/angrop/chain_builder.pyc in execve(self, target, addr_for_str)
    427         # TODO If this fails try using partial controllers
    428         chain2 = self.do_syscall(self._execve_syscall, [addr_for_str, 0, 0],
--> 429                                  use_partial_controllers=use_partial_controllers, needs_return=False)
    430         result = chain + chain2
    431 

/home/yans/code/angr/angrop/angrop/chain_builder.pyc in do_syscall(self, syscall_num, arguments, ignore_registers, modifiable_memory_range, use_partial_controllers, rebase_regs, needs_return)
    127 
    128         # first find gadgets to the set the registers
--> 129         chain = self.set_regs(modifiable_memory_range, use_partial_controllers, rebase_regs, **registers)
    130 
    131         # find small stack change syscall gadget that also fits the stack arguments we want

/home/yans/code/angr/angrop/angrop/chain_builder.pyc in set_regs(self, modifiable_memory_range, use_partial_controllers, rebase_regs, **registers)
     86 
     87         return self._build_reg_setting_chain(gadgets, modifiable_memory_range,
---> 88                                              registers, best_stack_change, rebase_regs)
     89 
     90     # TODO handle mess ups by _find_reg_setting_gadgets and see if we can set a register in a syscall preamble

/home/yans/code/angr/angrop/angrop/chain_builder.pyc in _build_reg_setting_chain(self, gadgets, modifiable_memory_range, register_dict, stack_change, rebase_regs)
    804                                                        endness=self.project.arch.memory_endness)
    805 
--> 806             val = test_symbolic_state.se.eval(sym_word)
    807 
    808             if len(rebase_regs) > 0:

/home/yans/code/angr/angr/angr/state_plugins/solver.pyc in eval(self, e, **kwargs)
    536         """
    537         # eval_upto already throws the UnsatError, no reason for us to worry about it
--> 538         return self.eval_upto(e, 1, **kwargs)[0]
    539 
    540     def eval_one(self, e, **kwargs):

/home/yans/code/angr/angr/angr/state_plugins/solver.pyc in eval_upto(self, e, n, cast_to, **kwargs)
    519             return [self._cast_to(e, concrete_val, cast_to)]
    520 
--> 521         cast_vals = [self._cast_to(e, v, cast_to) for v in self._eval(e, n, **kwargs)]
    522         if len(cast_vals) == 0:
    523             raise SimUnsatError('Not satisfiable: %s, expected up to %d solutions' % (e.shallow_repr(), n))

/home/yans/code/angr/angr/angr/state_plugins/solver.pyc in concrete_shortcut_tuple(self, *args, **kwargs)
    155         v = _concrete_value(args[0])
    156         if v is None:
--> 157             return f(self, *args, **kwargs)
    158         else:
    159             return ( v, )

/home/yans/code/angr/angr/angr/state_plugins/sim_action_object.pyc in ast_stripper(*args, **kwargs)
     51         new_args = _raw_ast(args)
     52         new_kwargs = _raw_ast(kwargs)
---> 53         return f(*new_args, **new_kwargs)
     54     return ast_stripper
     55 

/home/yans/code/angr/angr/angr/state_plugins/solver.pyc in wrapped_f(*args, **kwargs)
     86     def wrapped_f(*args, **kwargs):
     87         try:
---> 88             return f(*args, **kwargs)
     89         except claripy.UnsatError:
     90             e_type, value, traceback = sys.exc_info()

/home/yans/code/angr/angr/angr/state_plugins/solver.pyc in _eval(self, e, n, extra_constraints, exact)
    367         :rtype: tuple
    368         """
--> 369         return self._solver.eval(e, n, extra_constraints=self._adjust_constraint_list(extra_constraints), exact=exact)
    370 
    371     @concrete_path_scalar

/home/yans/code/angr/claripy/claripy/frontend_mixins/concrete_handler_mixin.pyc in eval(self, e, n, **kwargs)
      5             return (c,)
      6         else:
----> 7             return super(ConcreteHandlerMixin, self).eval(e, n, **kwargs)
      8 
      9     def batch_eval(self, exprs, n, **kwargs): #pylint:disable=unused-argument

/home/yans/code/angr/claripy/claripy/frontend_mixins/constraint_filter_mixin.pyc in eval(self, e, n, extra_constraints, **kwargs)
     38     def eval(self, e, n, extra_constraints=(), **kwargs):
     39         ec = self._constraint_filter(extra_constraints)
---> 40         return super(ConstraintFilterMixin, self).eval(e, n, extra_constraints=ec, **kwargs)
     41 
     42     def batch_eval(self, exprs, n, extra_constraints=(), **kwargs):

/home/yans/code/angr/claripy/claripy/frontend_mixins/sat_cache_mixin.pyc in eval(self, e, n, extra_constraints, **kwargs)
     54             r = super(SatCacheMixin, self).eval(
     55                 e, n,
---> 56                 extra_constraints=extra_constraints, **kwargs
     57             )
     58             self._cached_satness = True

/home/yans/code/angr/claripy/claripy/frontend_mixins/simplify_helper_mixin.pyc in eval(self, e, n, *args, **kwargs)
     11         if n > 1:
     12             self.simplify()
---> 13         return super(SimplifyHelperMixin, self).eval(e, n, *args, **kwargs)
     14 
     15     def batch_eval(self, e, n, *args, **kwargs):

/home/yans/code/angr/claripy/claripy/frontend_mixins/constraint_expansion_mixin.pyc in eval(self, e, n, extra_constraints, exact, **kwargs)
     10             extra_constraints=extra_constraints,
     11             exact=exact,
---> 12             **kwargs
     13         )
     14 

/home/yans/code/angr/claripy/claripy/frontends/composite_frontend.pyc in eval(self, e, n, extra_constraints, exact)
    279 
    280     def eval(self, e, n, extra_constraints=(), exact=None):
--> 281         self._ensure_sat(extra_constraints=extra_constraints)
    282 
    283         ms = self._merged_solver_for(e=e, lst=extra_constraints)

/home/yans/code/angr/claripy/claripy/frontends/composite_frontend.pyc in _ensure_sat(self, extra_constraints)
    257     def _ensure_sat(self, extra_constraints):
    258         if self._unsat or (len(extra_constraints) == 0 and not self.satisfiable()):
--> 259             raise UnsatError("CompositeSolver is already unsat")
    260 
    261     def satisfiable(self, extra_constraints=(), exact=None):

SimUnsatError: ('Got an unsat result', <class 'claripy.errors.UnsatError'>, UnsatError('CompositeSolver is already unsat',))

libc.tar.gz

[zardus]

Opening this here because my student has kindly volunteered to work on this :-)

[github-actions[bot]]

This issue has been marked as stale because it has no recent activity. Please comment or add the pinned tag to prevent this issue from being closed.

[github-actions[bot]]

This issue has been closed due to inactivity.