Boosting the efficiency of static program analysis using configuration tuning

An improved static program analysis procedure is provided by formulating a set of seeding configurations, and selecting a subset of queries posed by the static program analysis procedure. In response to one or more queries of the subset of queries being answered positively under at least one configuration of the set of seeding configurations, the one or more queries are determined to be valid queries. Each query of the valid queries is evaluated under each configuration of the set of seeding configurations to determine an accuracy score for each seeding configuration. A seeding configuration having a highest accuracy score is selected as a tool configuration to be used with the static program analysis procedure.

FIELD

The present application relates generally to code verification and, more particularly, to techniques for improving the efficiency of static program analysis methods.

BACKGROUND

Code verification and validation is the process of determining that a software program meets all specifications and fulfills its intended purpose. Code verification addresses the issue of the software program achieving its goals without any bugs or gaps. On the other hand, code validation ascertains whether or not the software meets high-level requirements and addresses the problem to be solved. Code verification ensures that “you built it right”. Code validation ensures that “you built the right thing”.

Static program analysis refers to analyzing computer software without actually executing the software. Static program analysis has been shown to be of great value in automating code verification tasks. Examples include functional verification tools such as Coverity™, as well as security analysis tools such as IBM Security AppScan Source Edition™ and HP Fortify 360™. One challenge faced by all tools based upon static program analysis is to achieve a proper balance between precision and scalability. Precision is achieved by building a granular albeit expensive analysis model. Scalability requires the opposite—a lightweight and less descriptive model.

A broad spectrum of parameters and models are available for determining the precision and scalability of the analysis tool. Some illustrative examples include a heap model, libraries and frameworks, virtual methods, path sensitivity, flow sensitivity, and reflection.

Heap Model: The heap model is based upon modeling dynamic memory allocation. This modeling process could lead to an unbounded number of runtime objects, and so the analysis must apply some type of finite approximation. The question of how to model runtime objects has received extensive treatment, resulting in many different heap modeling techniques. Some techniques are computationally cheap, such as Open Computer Forensics Architecture (OCFA). Others are computationally expensive, such as Three Valued Logic Analyzer (TVLA).

Libraries and Frameworks: The code to be considered in a given scope of analysis is primarily contributed by libraries and frameworks. For scalability, certain analyses model the effects of library calls conservatively via generic summaries. Other analyses that are more precise dive into the implementation to derive an accurate model of the library or framework's behavior.

Virtual Methods: Resolving virtual method calls is an undecidable problem in general. The difficulty relates to determining an exact identity of the object or objects flowing into the invocation site. Doing so precisely may involve abstraction refinement, demand-driven pointer analysis, on-demand interprocedural type inference, or another nontrivial technique. Alternatively, the analysis could make a conservative decision and resolve the invocation per all possible receiver abstractions.

Path Sensitivity: An important consideration is whether to explicitly model assertions following from branching along conditional and looping statements. Doing so undoubtedly enhances precision, but at the same time, a state space maintained by the analysis is split on every path condition. This can lead to a solution where a quantity is undefined or goes to infinity.

Flow Sensitivity: Another aspect is flow sensitivity which renders a decision as to whether or not to account for the order in which memory updates are performed. Naturally, flow insensitivity yields a much more scalable analysis compared to being flow sensitive.

Reflection: Similar to virtual calls, varying levels of precision may be provided in resolving reflective constructs, such as deciding a concrete identity of a type allocated via reflection. These processes involve both backward and forward traversal of a program's control structure to derive constraints on the behavior of a reflective statement (e.g., downstream downcasts).

The foregoing discussion indicates that the question of how to optimally balance between precision and scalability is naturally undecidable. It is impossible, in general, to compute a precise tradeoff between the two such that the analysis achieves the most accurate results without leading to a computer system crash. Thus, there exists a need to overcome at least one of the preceding deficiencies and limitations of the related art.

SUMMARY

A computer-executed method for providing an improved static program analysis procedure, in one aspect, comprises formulating a set of seeding configurations, selecting a subset of queries posed by the static program analysis procedure, each query of the subset of queries being directed to whether or not an operation or a subset of the operation is predicted to be executed safely; in response to one or more queries of the subset of queries being answered positively under at least one configuration of the set of seeding configurations, determining that the one or more queries are valid queries; evaluating each query of the valid queries under each configuration of the set of seeding configurations to determine an accuracy score for each configuration of the set of seeding configurations, and selecting a seeding configuration having a highest accuracy score among the set of seeding configurations as a tool configuration to be used with the static program analysis procedure.

A computer program product for providing an improved static program analysis procedure, in another aspect, comprises a non-transitory computer-readable storage medium having a computer-readable program stored therein, wherein the computer-readable program, when executed on a computer system comprising at least one processor, causes the computer system to formulate a set of seeding configurations, select a subset of queries posed by the static program analysis procedure, each query of the subset of queries being directed to whether or not an operation or a subset of the operation is predicted to be executed safely; in response to one or more queries of the subset of queries being answered positively under at least one configuration of the set of seeding configurations, determine that the one or more queries are valid queries; evaluate each query of the valid queries under each configuration of the set of seeding configurations to determine an accuracy score for each configuration of the set of seeding configurations, and select a seeding configuration having a highest accuracy score among the set of seeding configurations as a tool configuration to be used with the static program analysis procedure.

An apparatus for providing an improved static program analysis procedure, in another aspect, may comprise a processor and a non-transitory computer-readable memory coupled to the processor, wherein the memory comprises instructions which, when executed by the processor, cause the processor to formulate a set of seeding configurations, select a subset of queries posed by the static program analysis procedure, each query of the subset of queries being directed to whether or not an operation or a subset of the operation is predicted to be executed safely; in response to one or more queries of the subset of queries being answered positively under at least one configuration of the set of seeding configurations, determine that the one or more queries are valid queries; evaluate each query of the valid queries under each configuration of the set of seeding configurations to determine an accuracy score for each configuration of the set of seeding configurations, and select a seeding configuration having a highest accuracy score among the set of seeding configurations as a tool configuration to be used with the static program analysis procedure.

DETAILED DESCRIPTION

FIGS. 1A-1Btogether comprise a flowchart illustrating an exemplary method for performing static program analysis using configuration tuning. The procedure commences at block101where a time budget for configuration tuning is defined, specified, or selected. In general, system tuning refers to a process of optimizing a program or a system for a particular environment by adjusting one or more numerical parameters designed as hooks for tuning. One may optimize the tuning for time (fast execution), for space (least memory use), or in the present scenario, for a configuration that represents the most efficient use of hardware. Next, at block103, a set of seeding configurations Ci={C1, . . . Ck} is formulated and initialized. Then, at block105, a subset Q of queries posed by the static program analysis procedure is selected. Alternatively or additionally, all queries posed by the static program analysis procedure may be selected. Each query of the subset Q of queries is directed to whether or not an operation or a subset of the operation is predicted to be executed safely.

The operational sequence progresses to block107where, in response to one or more queries Qt=q1. . . qwof the subset of queries being answered positively under at least one configuration of the set of seeding configurations, the one or more queries Qt=q1. . . qware identified as valid queries. Next, at block109, each query of the valid queries is evaluated under each configuration of the set of seeding configurations to determine an accuracy score for each configuration Ciof the set of seeding configurations. The accuracy score is determined as follows. For each configuration Ci: If an ithconfiguration Cicauses the static program analysis procedure to crash or to time out, then the accuracy score for the ithconfiguration Ciis set to zero. Otherwise, the accuracy score for the ithconfiguration Ciis determined to be a proportion of the one or more identified valid queries Qt=q1. . . qwthat are answered positively under the ithconfiguration Ciwithin the subset Q of queries: |{q in Qt: q answered positively under Ci}|/|Q|.

At block111, a test is performed to ascertain whether or not the time budget for configuration tuning that was defined, specified, or selected at block101has been exceeded. If the time budget has not been exceeded, the program progresses to block113where a search heuristic is applied to define a new set of seeding configurations based upon the scores assigned to each of the configurations Ci. The program then loops back to block105.

The affirmative branch from block111leads to block115where a highest accuracy score among the set of accuracy scores is identified. Next, at block117, a seeding configuration of the set of seeding configurations Ciis identified that corresponds to the highest accuracy score. Then, at block119, the identified seeding configuration corresponding to the highest accuracy score among the set of seeding configurations is selected as a tool configuration to be used with the static program analysis procedure.

As mentioned previously, system tuning refers to a process of optimizing a program or a system for a particular environment by adjusting one or more numerical parameters designed as hooks for tuning. One may optimize the tuning for time (fast execution), for space (least memory use), or for a configuration that represents the most efficient use of hardware. In the present example, these numerical parameters are provided by using the seeding configuration having the highest accuracy score among the set of seeding configurations Ci.

The static program analysis procedure ofFIGS. 1A and 1Bmay be implemented using any analysis tool that is performed without actually executing the code of a software program under test. In some cases, the analysis is performed on source code, and in other cases, the analysis is performed on object code. In general, static program analysis takes place within a specific program or subroutine, without connecting to the context of that program.

Static program analysis may be performed on any of three basic levels. These include a technology level, a system level, and a mission/business level. The technology level takes into account interactions between a plurality of unit programs to obtain a holistic and semantic view of the overall program in order to locate issues and avoid obvious false positives. The system level takes into account interactions between unit programs, but without being limited to one specific technology or programming language. The mission/business level takes into account terms, rules and processes that are implemented within the software system for its operation as part of enterprise or program/mission layer activities. These elements are implemented without being limited to one specific technology or programming language and in many cases are distributed across multiple languages but are statically extracted and analyzed for system understanding for mission assurance.

Formal methods may be used to implement static program analysis. Formal methods refers to a category of analysis tools where results are obtained purely through the use of rigorous mathematical methods. Mathematical techniques such as denotational semantics, axiomatic semantics, operational semantics, abstract interpretation, or any of various combinations thereof may be employed. However, using formal methods to locate all possible run-time errors in an arbitrary program (or more generally any kind of violation of a specification on the final result of a program) is an undecidable problem. No mathematical method exists that can always answer truthfully whether an arbitrary program may or may not exhibit runtime errors. This result dates from the works of Church, Gedel and Turing in the 1930s. As with many undecidable questions, one can still attempt to provide useful approximate solutions.

In practice, formal static program analysis may be implemented using model checking, data-flow analysis, abstract interpretation, Hoare logic, symbolic expression, or any of various combinations thereof. Model checking considers software that has finite states, or that may be reduced to finite states by abstraction. Data-flow analysis is a lattice-based technique for gathering information about a possible set of values. Abstract interpretation models an effect that each of a plurality of statements has on a state of an abstract machine. The software is “executed” based on the mathematical properties of each statement. However, this abstract machine over-approximates the behaviors of the software. The abstract software is thus made simpler to analyze, at the expense of incompleteness. Not every property true of the original software will be true of the abstracted software. If performed properly, abstract interpretation is a sound technique. Every property true of the abstracted software can be mapped to a true property of the original software.

Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. Symbolic execution is another formal system that is used to derive mathematical expressions representing values for a plurality of mutated variables at particular points in the code.

With regard to block113(FIG. 1B), any of a variety of different methods may be used to guide the search for an effective configuration for any of the foregoing static program analysis tools, or for any other static program analysis tool not mentioned previously. Genetic algorithms represent one notable family of search techniques. Genetic algorithms belong to a larger class of algorithms called evolutionary algorithms which generate solutions to optimization problems using techniques inspired by biological natural evolution, such as inheritance, mutation, selection, and crossover.

In the field of artificial intelligence, a genetic algorithm is a search heuristic that mimics the process of natural selection. This heuristic (also sometimes called a metaheuristic) can be used to generate useful solutions to optimization and search problems. Pursuant to a genetic algorithm, a population of candidate solutions (called individuals, creatures, or phenotypes) to an optimization problem is evolved towards better solutions. Each candidate solution has a set of properties (its chromosomes or genotype) which can be mutated and altered. In some cases, solutions are represented in binary as strings of 0's and 1's, but other encodings are also possible.

The evolution towards better solutions may start from a population of randomly-generated individuals. Evolution is an iterative process, with the population in each iteration called a generation. In each generation, the fitness of every individual in the population is evaluated. The fitness is usually defined in terms of a value of an objective function in the optimization problem being solved. The individuals having the greatest fitness are stochastically selected from the current population, and each individual's genome is modified (recombined and possibly randomly mutated) to form a new generation. The new generation of candidate solutions is then used in the next iteration of the genetic algorithm. Illustratively, the genetic algorithm terminates when either a maximum number of generations has been produced, or a satisfactory fitness level has been reached for population.

The genetic algorithm requires defining a genetic representation of a solution domain, and formulating a fitness function to evaluate the solution domain. Once the genetic representation and the fitness function are defined, the genetic algorithm proceeds to initialize a population of solutions, and then to improve these solutions through repetitive application of mutation, crossover, inversion and selection operators. This generational process is repeated until a termination condition has been reached. Terminating conditions may comprise one or more of: a solution is found that satisfies minimum criteria; a fixed number of generations are reached; an allocated budget (in terms of computation time and/or money) is reached; the fitness of a highest ranking solution is reaching or has reached a plateau such that successive iterations no longer produce better results; manual inspection; or any of various combinations thereof.

As an alternative or addition to genetic algorithms, a technique called hill climbing may be used in conjunction with block113to guide the search for an effective configuration. In the field of computer science, hill climbing is a mathematical optimization technique which belongs to a family of techniques called local search. Hill climbing is an iterative algorithm that starts with an arbitrary solution to a problem, and then attempts to find a better solution by incrementally changing a single element of the solution. If the change produces a better solution, an incremental change is made to the new solution, repeating until no further improvements can be found.

Hill climbing attempts to maximize (or minimize) a target function ƒ(x), where x is a vector of continuous and/or discrete values. At each iteration, the hill climbing algorithm adjusts a single element in x and determines whether the change in this single element improves the value of ƒ(x). Note that this approach differs from gradient descent methods which adjust all of the values in x at each iteration according to a gradient of the hill. With hill climbing, any change that improves ƒ(x) is accepted, and the process continues until no change can be found to improve the value of ƒ(x). Then x is said to be “locally optimal”. In discrete vector spaces, each possible value for x may be visualized as a vertex in a graph. Hill climbing will follow the graph from vertex to vertex, always locally increasing or decreasing) the value of ƒ(x), until a local maximum local minimum) xmis reached.

For purposes of illustration, hill climbing can be applied to a travelling salesman problem where a salesman is required to visit a number of different cities. It is easy to find an initial solution where the salesman is scheduled to visits all of the cities, but this initial solution will likely be very poor and inefficient compared to an optimal solution. The hill climbing algorithm starts with such an initial solution and makes small incremental improvements to the solution, such as switching the order in which two cities are visited. Eventually, a much shorter and more efficient route is likely to be obtained.

The hill climbing algorithm is well suited for finding a local optimum in the form of a solution that cannot be improved upon only by considering a neighboring configuration. However, the hill climbing algorithm is not necessarily guaranteed to find a best possible solution (a global optimum) out of all possible solutions (a search space). In order to overcome this limitation, it is possible to use repeated local searches (restarts), or more complex schemes based on iterations, such as an iterated local search on memory, a reactive search optimization on memory, a tabu search, or a memory-less stochastic modification such as simulated annealing.

As an alternative or addition to genetic algorithms and hill climbing algorithms, a technique called simulated annealing may be used in conjunction with block113to guide the search for an effective configuration. Simulated annealing is a probabilistic technique for approximating a global optimum of a given function. Specifically, this technique is a metaheuristic to approximate global optimization in a large search space. Simulated annealing may be used when a search space is discrete. One illustrative example of a discrete search space comprises all tours that visit a given set of cities. For problems where finding the precise global optimum is less important than finding an acceptable local optimum in a fixed amount of time, simulated annealing may be preferable to alternatives such as brute-force search or gradient descent.

Simulated annealing exploits a property called slow cooling. Slow cooling refers to a slow decrease in the probability of accepting worse solutions as the technique progressively explores the solution space. Accepting worse solutions is a fundamental property of metaheuristics because it allows for a more extensive search for the optimal solution. The state of a physical system s, and a function E(s) to be minimized is analogous to an internal energy of the system in that state. The goal is to bring the system, from an arbitrary initial state, to a state with the minimum possible energy. At each step, the simulated annealing heuristic considers one or more neighboring states s′ of the current state s, and probabilistically decides between moving the system to state s′ or staying in state s. These probabilities ultimately lead the system to move to states of lower energy. The foregoing step is repeated until the system reaches a state that is good enough for the application, or until a given computation budget has been exhausted.

The neighbors of a state are new states of the problem that are produced after altering a given state in some well-defined way. For example, in the travelling salesman problem discussed previously, each state is typically defined as a permutation of the cities to be visited. The neighbors of a state are the set of permutations that are produced, for example, by reversing the order of any two successive cities. The well-defined way in which the states are altered in order to find neighboring states is called a “move” and different moves give different sets of neighboring states. These moves usually result in minimal alterations of the last state, as the previous example depicts, in order to help the simulated annealing algorithm retain the better parts of the solution and change only the worse, parts. In the traveling salesman problem, each respective part of the solution corresponds to a specific city-to-city connection.

Searching for neighbors of a state is fundamental to simulated annealing optimization because a final solution will be found after a tour of successive neighbors is performed. Simple heuristics move from neighbor to neighbor by finding a sequence of best neighbors, and the heuristics stop when a solution is reached which has no neighbors that are better solutions. One problem with this approach is that the neighbors of a state are not guaranteed to contain any of the existing better solutions. This means that failure to find a better solution among them does not guarantee that no better solution exists. This is why the best solution found by such algorithms is called a local optimum, in contrast with the actual best solution which is called a global optimum. Metaheuristics use the neighbors of a solution as a way to explore the solution space, and although the metaheuristics prefer better neighbours, the metaheuristics also accept worse neighbours in order to avoid getting stuck at a local optima. If the simulated annealing algorithm were run for an infinite amount of time, the global optimum would eventually be found.