angr: Add constraint on load address to state

0

This question pertains to the symbolic execution platform angr. Particularly, I want to ask two questions:

  1. How to find a symbolic expression for the address operand of a load instruction?
  2. How to add a constraint to a state, where the aforementioned address is a known value?

To give some more background, I am using the Simulation Manager, where at any point, there are a list of states in stashes. Let us consider any one particular state st0. This state stores the symbolic state as per the sequence of instructions leading up to the last instruction, say the load mov (rdx), rax. Now, external information (which angr does not have) has informed me that the address accessed is actually 0xdeadbeef.

Therefore, the steps I think I need to do are:

  1. From s0.addr, figure out the instruction, and its address operand. From this, I get a symbolic bitvector for s0.regs._rax. The question is basically, how do I figure out that the address used by the load was rax?
  2. Add the constraint that rax == 0xdeadbeef. Thankfully, angr state has a nice add_constraint function. The question is, how do I express my constraint in code?
python
symbolic-math
angr
asked on Stack Overflow Jul 13, 2020 by TSG

0 Answers

Nobody has answered this question yet.


User contributions licensed under CC BY-SA 3.0