Detecting exploitable bugs in binary code
AssigneeCarnegie Mellon University
InventorsDavid Brumley, Sang Kil Cha, Thanassis Avgerinos, Alexandre Rebert
Life of this patent
Estimating the term…
Abstract
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.
Claims22
A system comprising:
- a hardware memory;
- and
- one or more hardware processors coupled to the hardware memory and configured to perform operations comprising:
- selecting a portion of a symbolic memory resource based on an analysis of symbolic memory cells of the symbolic memory resource;
- by symbolic execution, determining a set of values that are referenced by the selected portion of the symbolic memory resource;
- performing symbolic execution of a target program by utilizing the determined set of values that are referenced by the selected portion of the symbolic memory resource, the performing of the symbolic execution including causing the symbolic execution to switch from a first mode to a second mode, the first mode using multiple interpreters at a branch point in the execution path and continuing the symbolic execution after the branch point without symbolic re-execution of any portion of the execution path prior to the branch point, the second mode initiating a separate symbolic execution of the target program in response to the branch point in the execution path;
- and
- creating an input formula for the target program based on the performed symbolic execution that switched from the first mode to the second mode.
A method comprising:
- using at least one processor, selecting a portion of a symbolic memory resource based on an analysis of symbolic memory cells of the symbolic memory resource;
- using at least one processor, by symbolic execution, determining a set of values that are referenced by the selected portion of the symbolic memory resource;
- performing symbolic execution of a target program by utilizing the determined set of values that are referenced by the selected portion of the symbolic memory resource, the performing of the symbolic execution including causing the symbolic execution to switch from a first mode to a second mode, the first mode using multiple interpreters at a branch point in the execution path and continuing the symbolic execution after the branch point without symbolic re-execution of any portion of the execution path prior to the branch point, the second mode initiating a separate symbolic execution of the target program in response to the branch point in the execution path;
- and
- creating an input formula for the target program based on the performed symbolic execution that switched from the first mode to the second mode.
A non-transitory computer-readable storage medium comprising instructions that, when executed by one or more processors of a computer, cause the computer to perform operations comprising:
- selecting a portion of a symbolic memory resource based on an analysis of symbolic memory cells of the symbolic memory resource;
- by symbolic execution, determining a set of values that are referenced by the selected portion of the symbolic memory resources;
- performing symbolic execution of a target program by utilizing the determined set of values that are referenced by the selected portion of the symbolic memory resource, the performing of the symbolic execution including causing the symbolic execution to switch from a first mode to a second mode, the first mode using multiple interpreters at a branch point in the execution path and continuing the symbolic execution after the branch point without symbolic re-execution of any portion of the execution path prior to the branch point, the second mode initiating a separate symbolic execution of the target program in response to the branch point in the execution path;
- and
- creating an input formula for the target program based on the performed symbolic execution that switched from the first mode to the second mode.
Dependencies are inferred from the claim text.