Part 35 Buffer Overflow

Concolic Execution

Combining Real and Symbolic Execution to Discover New Paths

Concolic Execution
is a combination of two methods:

Concrete Execution:
Executing the program with real input

Symbolic Execution:
Symbolically examining the data and conditions of the execution path

The goal is to start from a real execution, extract the conditions that the program has passed and create new inputs so that other paths can be examined

A simple example

Suppose the program is:

int check(int x)
{
if (x > 10)
{
if (x < 20)
return 1;
}

return 0;
}

We execute the program with this input:

x = 5

Since the condition "x > 10" is not true, the program goes directly to "return 0"

Execution path:

x = 5
|
x > 10 ?
|
False
|
return 0

So far we have only examined one path

But Concolic Execution can use the same execution to find new inputs

Extracting Path Condition

In the above execution, the following condition is examined:

if (x > 10)

The actual value of "x" is 5, so the condition is false

The symbolic constraint of the path taken is:

x <= 10

Now, to examine the opposite branch, we consider this condition:

x > 10

A constraint solver such as SMT Solver can suggest a suitable value:

x = 15

By re-executing the program:

x = 15
|
x > 10 ?
|
True
|
x < 20 ?

This time we reached the second condition, a path that we had not reached in the previous execution

Create a new input for the next path

The second condition is:

if (x < 20)

For input 15, this condition is also met and the program reaches this section:

return 1;

The constraints of the successful path of this program are:

x > 10
AND
x < 20

That is:

10 < x < 20

So "x = 15" is a valid input to reach this path

The important point is that the new input is not chosen randomly but is created using path constraints

In practice, the tool can record the executed paths and create a new input to reach a different branch by changing one of the conditions

General Algorithm of Concolic Execution

Program Execution

The program is executed with a real input

Recording Path Constraints

The tool records the conditions of the branches that the program has crossed. These conditions are called "Path Constraints".
Changing a Path Condition

Changes one of the conditions to check the opposite branch while still considering the previous path conditions

Resolving Constraints

An "SMT Solver" tries to find an input that satisfies the new conditions

Rerun with new input

The program is re-executed with the given input to check a different path

This cycle can be repeated many times to cover more paths

Relationship of Concolic Execution to Fuzzing

In typical Fuzzing, inputs are often created by mutating or changing previous inputs

For example:

Input A
↓
Mutation
↓
Input B
↓
New Execution

But sometimes the program has a condition that makes it difficult to reach the desired branch

For example:

if (input[0] == 'R' &&
input[1] == 'E' &&
input[2] == 'V')
{
process_special_case();

}

Fuzzer
must find an input that satisfies all three conditions

Concolic Execution
can analyze the conditions examined and suggest suitable inputs to traverse the branches

Input
↓
Execution
↓
Path Constraints
↓
Solver
↓
New Input
↓
New Path

This idea is used in Concolic Testing and some intelligent input guidance methods in software testing

Of course, modern fuzzers can also use techniques such as "Coverage-Guided Fuzzing" and reach new paths with targeted jumps without solving the conditions symbolically

Limitations of this method

Concolic Execution
is not magic, although its name seems to be explaining its program to us

It has several important problems:

Path Explosion:
The number of possible paths can increase rapidly

Solver Limitations:
Some conditions, especially complex calculations or operations Unsupported may be difficult to solve

Execution Dependency:
Analysis usually starts with paths that require proper inputs to be generated with the initial execution to reach other paths