Optimization Tips

Mark Mossberg edited this page Aug 8, 2017 · 5 revisions

Modeling functions

See here: http://manticore.readthedocs.io/en/latest/models.html

Patching out functions

For example, printf could be a pretty expensive function to symbolically execute, but doesn't actually affect the program. You can use a manticore hook to effectively patch it out.

def patch_printf(state):
  state.cpu.PC = address_of_printf_ret
  # state.cpu.RAX = some_return_value (if you also care about the function's return value (maybe strlen?), just set the appropriate register to it!)

Abandoning irrelevant states

The state.abandon() API is really useful for making an analysis run faster. If you know that you aren't interested in certain code paths, hook on them, and simply just call state.abandon().

Adding temporary constraints

Manticore supports adding temporary constraints that would otherwise overconstrain the state to aid in solving. For example (from state.solve_buffer)

buffer = self.cpu.read_bytes(addr, nbytes)
result = []
with self.constraints as temp_cs:
    for c in buffer:
    result.append(self._solver.get_value(temp_cs, c))
    temp_cs.add(c == result[-1])
return result
# No constraints are actually added to state.constraints!

Similarly, you can use with state as temp_state: ..., but only changes to state.constraints will be local to the with block.

state.mem.write(addr, 'a')
with state as temp_state:
    temp_state.mem.write(addr, 'b')
state.mem.read(addr, 1) # ['b']!