return 0;
}
Standard analysis reveals that the program has several conditions.
However, Symbolic Execution can extract the conditions necessary to reach a successful execution path:
value >= 100
AND
value <= 200
AND
value == 150
Consequently,
value = 150
is a valid solution.
This capability has significant applications in reverse engineering:
Analyzing validation logic
Finding the inputs required to reach a specific path
Examining complex conditions within the binary
Analyzing paths that lead to a crash
Determining which constraints make a path reachable or unreachable
Of course, in a real binary, conditions might depend on multiple functions or be influenced by memory and runtime state.
In such scenarios, constructing an accurate model of the program becomes more difficult.
The difference between Symbolic and Concrete Execution
Make sure to understand this distinction well.
Concrete Execution
The program runs with a concrete (actual) value.
x = 15
In this case, program processing is based on the actual value of 15.
Symbolic Execution
Instead of a concrete value, we use a symbolic value.
x = X
When conditions are encountered, constraints are generated for X.
A simple comparison
An important point
Symbolic Execution
does not guarantee that all program paths will be examined.
Loops and a large number of branches can lead to a "path explosion." 😁
Complex calculations and interactions with the operating system or external libraries can also complicate the analysis.
So, even Symbolic Execution has its own limitations.
Connection to Fuzzing
This is where Symbolic Execution demonstrates one of its most interesting applications.
Suppose a fuzzer has generated an input and executed the program:
Input
↓
Program
↓
Branch A
↓
Branch B ↓
Crash
Now, let's examine a new execution path—one that wasn't reached because a specific condition wasn't met.
For instance, the program contains a condition like this:
JavaScript
if (x == 1337)
dangerous_function(); If our current input is:
x = 10
The program does not enter
dangerous_function.Symbolic Execution
can extract the branch condition:
X == 1337
Then, the solver suggests a valid value:
X = 1337
This value can be used as a new input in the testing process.
So, the overall workflow looks like this:
Fuzzer
↓
Input
↓
Program Execution
↓
Uncovered Branch
↓
Path Constraint
↓
SMT Solver
↓
New Input
↓
Fuzzing Again
This concept is also utilized in methods like Concolic Execution.
In Concolic Execution, the program runs with concrete inputs while values and conditions are simultaneously tracked symbolically; thus, concrete execution and symbolic analysis are combined.
Practical Tools
To gain hands-on experience with this topic, a few tools are worth exploring:
angr
A binary analysis framework featuring capabilities such as Symbolic Execution and path analysis.
Official repository:
https://github.com/angr/angr
Triton
A framework for Dynamic Binary Analysis that offers capabilities like Taint Analysis and Symbolic Execution.
Official repository:
https://github.com/JonathanSalwan/Triton
Z3
An SMT solver capable of solving symbolic constraints.
Official repository:
https://github.com/Z3Prover/z3
These tools do not perform exactly the same function:
angr
Is primarily used for constructing and analyzing symbolic paths within binaries.
Triton
Provides capabilities for dynamic binary analysis and symbolic computation.
Z3
Is a constraint solver; while it is not a standalone, all-in-one tool for analyzing binary execution paths, it is a crucial component of such systems. It’s not possible [to do it that way].
The general workflow
of Symbolic Execution looks like this:
Symbolic Input
↓
Program Analysis
↓
Branch Conditions
↓
Path Constraints
↓
SMT Solver
↓
Possible Input
