The dream of defect-free software development! The reality of SPARROW- A semantic-based static program analysis engine.
Background
For last 25 years, computing power has been increased from 10^4 to 10^6. This is the same factor that the distance between Paris and Nice becomes the distance between the earth and the Mars. The size of program has also been expanded to about 400 files in average C programs.
The complexity of program has, in turn, been increased dramatically, which results in the increase of difficulties in bug detection / prevention. The boost of the program quality assurance cost seems almost inevitable. Today, the goal of program quality assurance is to find as many as defects, as early as possible, and as accurate as it can.
Especially, memory related defects cause malfunction of system or abrupt system stops. These accidents will lead to customers' dissatisfaction to the product as well as tremendous cost for locating and fixing the cause.
Static code analysis has been developed to address these issues. Static program analysis can uncover the vulnerabilities occurred in memory processing so that it can reduce the program quality assurance cost incredibly.
Program Analysis Overview
- The Competitiveness of SPA
Semantic-based SPA
Summary
Semantic-based static program analysis is to computes finitely the dynamics of a program without actually executing it. The analysis is performed in an abstract space, economically tracing all the execution paths of the program to determine properties of its behavior. Through the in-depth studies on the technology for last 30 years, now it is about to blossom its potential in the industry applications.
- Abstract Interpretation
- SPARROW uses a technology named "abstract interpretation", which summarizes the real execution path and put it into practice.
At first, the executions and the status of a programs are represented by graph. Nodes of graph indicates program status at the corresponding program points, and edges represents the execution flow. Suppose that the execution behavior of input program is described as the graph below. The first sequence branches to the left, the second to the right, and the third iterates the right branch four times.
There are almost infinite situations that a program may have depending on the input values. It is not possible to look into all the possibilities or even it's possible, it takes too much time and cost. To address this problem, SPARROW summarizes all the execution path of program and abstracts the situations finitely. However, this approximation may cause a "false positive", i.e. a defect alarm which is not true.
The picture below shows conceptually how the real program execution can be summarized to a finite graph. The core technology of abstract interpretation is to define how the summarized graph covers all the execution result.
Program Analysis
The analysis can be described as solving a set of equations defined by the abstract graph within finite time.
As described above, the graph represents the semantic of the input program and the nodes, program status at the corresponding program point. Therefore, it is possible to extract a set of equations in which the nodes become the unknows. The final status of program will be obtained by solving the equations (by fixed point iterations). SPARROW then analyzes the solutions for detecting the defects.
