Goanna Technology
Goanna is the result of many years of scientific research. It is the first static analysis tool for C/C++ using advanced model checking technology.
Model Checking Technology
Model checking is a Turing award winning technology that explores very large graphs in a highly efficient way for specified properties of interest. It has first been applied to verify digital circuits scaling to millions of elements. In the semi-conductor world model checking is a de facto standard for deep verification of crucial system design.
Model Checking in Static C/C++ Analysis
Goanna makes use of model checking technology by constructing for each C/C++ function a control low representation including information of interest. Such information can be facts about where memory is alloceted, where it is freed, where it is read from and written to. These locations of interest are mapped to the control flow structure and model-checking technology is then used to evaluated automatically whether, e.g., there is a path in the program such that memory is nor freed or freed memory is still accessed later on.
Model checking technology enables a path-sensitive precise analysis of all functions and efficiently handles hundreds of checks and variables at the same time, making it ideal for a fast and precise analysis.
Interprocedural Analysis
Another patent pending core technology of the Goanna static analysis tools is the ability to efficiently analysis whole-program data flow and dependencies. Imagine you have a function that assigns the NULL value to a pointer p. This pointer p is then passed a parameter to a function f and later from f to a function g. It is only that in g the pointer p finally gets first touched and dereferenced.The resulting null-pointer dereference is hard to spot by other means such as code reviews while the Goanna technology automatically detects these serious issues.
Internally, the tool constructs sophisticated summaries for each function and propagates those summaries with little overhead across the call graph. By enabling interprocedural analysis in Goanna Studio all the new information gets included in existing checks, making them in essence more precise.
Abstract Data Tracking
Goanna not only tracks information along the control flow and across functions, but it also computes possibly ranges for all integer values on the fly. An example is shown in the source code on the right. In this code Goanna knows about the size of the array, the different conditionals, the short circuit operator etc. and computes the min and max values based on the implicit constraints. As such it can report that there is a buffer overflow in the lst a[x] access but not in the other accesses.
Moreover, Goanna keeps track of possible min and max values even under basic arithmetic with other variables. This includes addition/subtraction and multiplication operation. The gained information is also used to discard paths in the program which are infeasible.
Background
The Goanna technology is the result of five years of scientific research at NICTA, Australia's largest dedicated IT research center. Goanna's model checking solution was designed with a number of advantages in mind, such as:
- superior speed/precision ratio
- fully automatic
- high flexibility for adding more checks
- scales well with additional checks and
- evaluation engine targeting 100% path coverage.
