Part 34 Buffer Overflow
Symbolic Execution
From Concrete Inputs to Symbolic Inputs
So far, we have learned how to trace data through a program and understand how it leads to a crash.
Now, let's take it a step further.
Imagine a program has a conditional statement that directs execution along a specific path only when the input holds a particular value.
We could try thousands of different inputs until we finally reach that path.
However, there is a better way.
Instead of testing only concrete values, we can use *Symbolic Execution* to determine the conditions that must be met for the program to enter the desired path.
Here, rather than guessing inputs, we attempt to extract and solve the path constraints.
What is the core idea?
Suppose we have the following program:
C
int check(int x)
{
if (x == 1337)
return 1;
return 0;
}
During a standard execution, we might provide this value:
x = 10
The program checks the condition:
10 == 1337
The result is false, and the program follows the second path.
Now, suppose we use a symbolic value instead of a concrete one:
x = X
In this case, the program's condition becomes:
X == 1337
A solver can deduce that for the program to enter the first path, the value of X must be 1337.
Thus, instead of testing various values, we can determine the necessary condition to reach that path.
Path Constraint
Suppose we have this code:
C
int process(int x)
{
if (x > 10)
{
if (x < 20)
return 1;
}
return 0; }
To reach
return 1, both conditions must be met:
x > 10
AND
x < 20
We refer to the set of conditions that must hold true to reach a specific path as a
Path Constraint
So, the constraint for the path in question is:
10 < x < 20
Since
x is of type
int, the possible solutions include these values:
11, 12, 13, 14, 15, 16, 17, 18, 19
The solver can find one of the valid solutions
For example:
x = 15
An important point is that Symbolic Execution does not consider only the current condition;
it also maintains the path's preceding conditions,
because reaching a specific point in the program requires all necessary conditions along the path to be satisfied.
When paths branch out
Consider this program:
C
int process(int x)
{
if (x > 10)
return 1;
if (x == 5)
return 2;
return 0;
}
Using Symbolic Execution, we can examine the program's various paths:
x = X
|
x > 10 ?
/ \
Yes No
| |
return 1 x == 5 ?
/ \
Yes No
| |
return 2 return 0
Now, suppose we want to reach the
return 2 statement.
First, the initial condition must *not* hold:
X <= 10
Then, the second condition *must* hold:
X == 5
So, our path constraint becomes:
X <= 10
AND
X == 5
Consequently:
X = 5
...is considered a valid input to reach this path.
This is the core idea behind Symbolic Execution:
We trace the program and gather the necessary conditions for each path.
The Role of the SMT Solver
So far, we’ve seen that we can extract path conditions, but solving them manually becomes difficult when the number of conditions grows.
This is where we use a tool called an
SMT Solver.
One well-known tool in this field
is Z3,
developed by Microsoft Research.
Suppose our conditions are:
X > 10
X < 20
X != 15
The solver must find a value that satisfies all conditions simultaneously.
For example:
X = 11
This value is valid because it satisfies all three conditions.
However, if the conditions were:
X > 20
X < 10
No real value could satisfy both conditions at the same time.
Consequently, the problem is
Unsatisfiable;
meaning there is no valid solution.
Conversely, if at least one solution exists, the problem
is considered Satisfiable.
Of course, SMT solvers aren't limited to simple numerical conditions.
Depending on the logic and capabilities of the solver, they can also handle constraints involving bit-vectors and bitwise operations.
