Detecting exploitable bugs in binary code
Systems and methods for performing hybrid symbolic execution to detect exploitable bugs in binary code are described. In some example embodiments, the systems and methods determine that resources associated with an execution client performing symbolic execution of a target program are below, at, or above a threshold performance level, generate checkpoints for active executing paths of the online symbolic execution, and cause the execution client to perform symbolic execution in response to the determination that the resources are at or above the threshold performance level.
1. A system, comprising:
a memory; and
one or more processors coupled to the memory and configured to:
monitor resources associated with an execution client performing symbolic execution of a target program that has a beginning, multiple execution paths, and multiple branch points among the multiple execution paths of the target program;
generate checkpoints for active symbolic execution paths of the symbolic execution;
cause the execution client to switch from a first mode of symbolic execution to a second mode of symbolic execution based on a performance level of the monitored resources, the execution client in the first mode being configured to fork multiple interpreters at a branch point encountered among the multiple branch points in symbolically executing an execution path among the multiple execution paths of the target program, the execution client in the first mode being configured to continue symbolic execution after the branch point without symbolic re-execution of any portion of the execution path prior to the branch point, the execution client in the second mode being configured to start a separate symbolic execution of the target program from the beginning for each branch point encountered in symbolically executing an execution path among the multiple execution paths of the target program;
restore the generated checkpoints by executing the target program using a path predicate for at least one checkpoint, the path predicate specifying conditions to execute a symbolic execution path to the at least one checkpoint; and
detect at least one bug based on the performed symbolic execution of the target program.
2. The system of claim 1 , wherein:
the one or more processors are further configured to
identify the active executing path based on the execution of the target program using the path predicate.
3. The system of claim 1 , wherein:
the one or more processors are further configured to restore the generated checkpoints by concretely executing the target program using one satisfiable assignment of the path predicate associated with the checkpoint until the target program reaches the instruction when a previous execution state was suspended.
4. The system of claim 1 , wherein:
the one or more processors are configured to detect an exploitable bug among the at least one bug based on the performed symbolic execution of the target program.
5. The system of claim 1 , wherein:
the one or more processors are further configured to automatically generate at least one exploit based on the detected at least one bug.
6. The system of claim 1 , wherein the performance level of the monitored resources is below a minimum threshold performance level.
7. The system of claim 1 , wherein the performance level of the monitored resources is at or above a cap performance level.
8. A computer-implemented method, comprising:
using at least one processor, monitoring resources associated with an execution client performing symbolic execution of a target program that has a beginning, multiple execution paths, and multiple branch points among the multiple execution paths of the target program;
generating checkpoints for active symbolic execution paths of the symbolic execution;
causing the execution client to switch from a first mode of symbolic execution to a second mode of symbolic execution based on a performance level of the monitored resources, the execution client in the first mode being configured to fork multiple interpreters at a branch point encountered among the multiple branch points in symbolically executing an execution path among the multiple execution paths of the target program, the execution client in the first mode being configured to continue symbolic execution after the branch point without symbolic re-execution of any portion of the execution path prior to the branch point, the execution client in the second mode being configured to start a separate symbolic execution of the target program from the beginning for each branch point encountered in symbolically executing an execution path among the multiple execution paths of the target program;
restoring the generated checkpoints by executing the target program using a path predicate for at least one checkpoint, the path predicate specifying conditions to execute a symbolic execution path to the at least one checkpoint; and
detecting at least one bug based on the performed symbolic execution of the target program.
9. The method of claim 8 , further comprising:
identifying the active executing path based on the execution of the target program using the path predicate.
10. The method of claim 8 , wherein further:
the restoring of the generated checkpoints includes concretely executing the target program using one satisfiable assignment of a path predicate associated with the checkpoint until the target program reaches the instruction when a previous execution state was suspended.
11. The method of claim 8 , wherein:
detecting an exploitable bug among the at least one bug based on the performed symbolic execution of the target program.
12. The method of claim 8 , further comprising:
automatically generating at least one exploit based on the detected at least one bug.
13. The method of claim 8 , wherein the performance level of the monitored resources is below a threshold performance level.
14. The method of claim 8 , wherein the performance level of the monitored resources is at or above a cap performance level.