Goanna Technology
The Goanna tool is the only static analysis tool for C/C++ based on advanced model checking technology.
The Problem
Automatic software analysis is hard. To have a precise, scalable and fast solution is even harder. Even within a single function there can be 100s of different potential execution paths, there can be 100s of variables that need to be considered simultaneously and all this has to be considered for a vast number of different checks.
Model Checking Technology
Model checking is a Turing award winning technology that explores very large annotated 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.
The Solution
Goanna is the first static analyzer that leverages model checking technology for statically analyzing C/C++ source code. This patent pending solution maps C/C++ source code to a graphical representation, often its control flow graph that is automatically annotated with points of interest. For instance, the annotation describe where memory is allocated, de-allocated and used. Based on this Goanna's model checking engine explores all paths automatically, checking, e.g., if there is a path such that previously allocated memory is still used after de-allocation.
Goanna's model checking solution has a number of advantages, such as:
- superior speed
- fully automatic
- high flexibility for adding more checks
- scales well with additional checks and
- symbolic evaluation engine guarantees 100% path coverage.
The Result
Goanna is a fast, scalable and precise software solution that detects bugs and vulnerabilities automatically at development time. Goanna’s patent pending technology allows it to analyze increasingly complex code by identifying causal dependencies and estimating all behaviors of a program. Goanna targets serious programming flaws such as memory corruption, buffer overruns, and memory leaks, which lead to potential system crashes or security intrusions.
For most programs the analysis takes just minutes, for some files often only fractions of a second. This is in stark contrast to traditional testing, which requires execution of the code, setup of test cases, and manual inspection of the test results against the specification. Goanna can be applied as soon as code compiles, well before the traditional testing phase (and without the requirement for test harnesses and stub code) which creates an enormous saving potential.
