-
Notifications
You must be signed in to change notification settings - Fork 0
Execution Engine
The backbone of Reilex is the symbolic execution engine.
The basic outline of symbolically executing a basic block is as follows:
- Load state from before the first instruction is executed.*
- Iterate over the REIL instructions in that basic block, at each step:
a.Load the symbolic value of each operand from the current state
b.Apply the REIL instruction**
c.Update the state according to the results of the REIL instruction
3.Upon reaching the end of the block, defer to the pathing strategy to determine next action.
*State consists of bindings between names of registers/memory addresses and an abstract syntax tree representing the symbolic value of the register/memory at the address. The implementation is simply a python dictionary such that the keys are names of registers/memory dresses and values are the abstract syntax trees.
**Implementation note: This is handled by a dictionary binding the names of operations to a pointer to a function that handles the operation. I believe this is a clean implementation, however it does require a separate function for each possible instruction. Since the semantics of REIL are so simple, this is acceptable.