By statically analyzing the program, we can create a system of constrained branches, and apply it to our input to explore interesting execution paths. It is approaching a program by viewing it as a set of branching paths, rather than analyzing it input by input.
Process
https://www.youtube.com/watch?v=yRVZPvHYHzw
- Treat the inputs as symbolic values
- When we encounter a conditional that affects the symbol, we use it to create a constraint and apply it to our symbol
- The split the path into 2, for both possible paths of execution Once, we find a branch that leads to a desired execution path, we evaluate the input constraints that lead us there. Sometimes the input that lead us to a path may have many values, or may be unsatisfiable. If a challenge is written correctly, we should have only 1 input.
Tools
Flaws
- Can lead to path explosion in larger programs. This is why you want angr to analyze as little as possible
Dynamic Symbolic Execution (Concolic Analysis)
A mix between symbolic and concrete execution. Execute what you can concretely, and use symbolic execution for certain segments