System and method for overflow detection using symbolic analysis

#Buffer overflows are a common cause of security vulnerabilities in systems code. Specifically, buffer overflow occurs when a process stores data in a buffer outside of the memory allocated for the process. The overflow can cause diverse errors including erratic program behavior, memory access errors, incorrect results, program crashes, and security breaches. A variety of techniques have been used to attempt to locate buffer overflows in code before they occur, including both dynamic and static techniques. One such technique is symbolic analysis.

#Symbolic analysis was originally introduced more than 30 years ago, and has been applied in a variety of manners such as parallelization, optimization, and bug detection. The symbolic expressions resulting from symbolic analysis are typically so large and complex that external mathematical libraries are needed to solve them. As expected, these complex expressions cause symbolic analysis to be of limited use when dealing with large amounts of variables and/or large amounts of code, due to the time required to process the code. While various techniques have been developed to speed up the symbolic analysis processes, the efficiencies gained from the various techniques typically come at the cost of less accurate results.

#In general, in one aspect, the invention relates to a method for demand-driven symbolic analysis. The method involves obtaining, using a processor, a section of code including a first instruction from a source code file, determining, using the processor, a critical variable in the section of code, determining, using the processor, data dependencies related to the critical variable, iteratively computing, using the processor, a symbolic value representing a first range of values of the critical variable according to the data dependencies, determining, using the processor, a first set of control predicates relevant to the critical variable at the first instruction, refining, using the processor, the first range of values according to the first set of control predicates to generate a second range of values for the symbolic value, and reporting, using the processor, an error when the second range of values exceeds a predetermined value.

#FIG. 1 shows a diagram of a system in accordance with one or more embodiments of the invention.

#FIG. 2 shows a flowchart of a method in accordance with one or more embodiments of the invention.

#FIGS. 3A-B show an example in accordance with one or more embodiments of the invention.

#Specific embodiments of the invention will now be described in detail with reference to the accompanying figures. Like elements in the various figures are denoted by like reference numerals for consistency.

#In the following detailed description of embodiments of the invention, numerous specific details are set forth in order to provide a more thorough understanding of the invention. However, it will be apparent to one of ordinary skill in the art that the invention may be practiced without these specific details. In other instances, well-known features have not been described in detail to avoid unnecessarily complicating the description.

#In general, embodiments of the invention provide a system and method for overflow detection. Specifically, in one or more embodiments of the invention, the method analyzes code prior to execution of the code, and determines if an overflow may occur by using symbolic analysis. The symbolic analysis is performed by determining critical variables in the code, and then defining symbolic values to represent the critical variables. More specifically, both data dependencies and control dependencies are used to iteratively compute the symbolic values of the critical variables for different instructions of the code. Initially, for a given instruction, a symbolic value for a critical variable may first be computed by considering the data dependencies of the critical variable. The symbolic value may then be refined using the control dependencies that are relevant to the critical variable.