[vc_row row_type=”row” type=”full_width” icon_pack=”font_awesome” content_menu_fe_icon=”arrow_back” text_align=”left” background_color=”#ffffff”][vc_column width=”1/1″][vc_row_inner row_type=”row” type=”grid” text_align=”left” padding_top=”65″][vc_column_inner width=”1/3″][vc_single_image image=”22341″ border_color=”grey” img_link_target=”_self” img_size=”full” css=”.vc_custom_1425276668486{padding-top: 20px !important;}”][/vc_column_inner][vc_column_inner width=”2/3″][vc_separator type=”transparent” position=”center” up=”15″ down=”0″][vc_column_text]

Goanna Engine Technology

[/vc_column_text][vc_separator type=”transparent” position=”center” up=”40″ down=”0″][vc_column_text]The core of the multi-patented Goanna analysis engine is the result of almost a decade of research into software verification and static program analysis at NICTA, Australia’s centre of excellence for IT research.

 

Goanna incorporated a range of verification techechnologies, including software model checking, data flow and taint analysis, abstract interpretation, and SMT solving.[/vc_column_text][vc_separator type=”transparent” position=”center” up=”60″ down=”0″][/vc_column_inner][/vc_row_inner][/vc_column][/vc_row][vc_row row_type=”row” use_row_as_full_screen_section=”no” type=”grid” icon_pack=”font_awesome” content_menu_fe_icon=”arrow_back” text_align=”left” background_color=”#f5f5f5″][vc_column width=”1/1″][vc_row_inner row_type=”row” type=”grid” text_align=”left” padding_top=”65″ use_row_as_full_screen_section_slide=”no”][vc_column_inner width=”2/3″][vc_separator type=”transparent” position=”center” up=”15″ down=”0″][vc_column_text]

Model Checking

[/vc_column_text][vc_separator type=”transparent” position=”center” up=”40″ down=”0″][vc_column_text]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 a control flow representation for each C/C++ function annotated with information of interest. Such information can be facts about where memory is; allocated, freed, read from, and written to. These locations of interest are mapped to the control flow structure and model checking technology is then used to check properties; e.g. if there is a path through the program where memory is not freed.

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 fast and precise analysis.

[/vc_column_text][vc_separator type=”transparent” position=”center” up=”60″ down=”0″][/vc_column_inner][vc_column_inner width=”1/3″][vc_single_image image=”22272″ border_color=”grey” img_link_target=”_self” img_size=”medium” alignment=”center” css=”.vc_custom_1424835794716{padding-top: 15px !important;}”][/vc_column_inner][/vc_row_inner][/vc_column][/vc_row][vc_row row_type=”row” type=”full_width” icon_pack=”font_awesome” content_menu_fe_icon=”arrow_back” text_align=”left” background_color=”#ffffff”][vc_column width=”1/1″][vc_row_inner row_type=”row” type=”grid” text_align=”left” padding_top=”65″][vc_column_inner width=”1/3″][vc_single_image image=”22273″ border_color=”grey” img_link_target=”_self” img_size=”medium”][/vc_column_inner][vc_column_inner width=”2/3″][vc_separator type=”transparent” position=”center” up=”15″ down=”0″][vc_column_text]

Abstract Interpretation

[/vc_column_text][vc_separator type=”transparent” position=”center” up=”40″ down=”0″][vc_column_text]Goanna not only tracks information along the control flow and across functions, but also computes possible ranges for many values on the fly. An example is shown in the source code on the right. Here Goanna determines the size of the array, the different conditions, the short circuit operator etc. and computes the min and max values based on the implicit constraints. As such Goanna can report that there is a buffer overflow in the last a[x] access but not in the others.

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.[/vc_column_text][vc_separator type=”transparent” position=”center” up=”60″ down=”0″][/vc_column_inner][/vc_row_inner][/vc_column][/vc_row][vc_row row_type=”row” use_row_as_full_screen_section=”no” type=”grid” icon_pack=”font_awesome” content_menu_fe_icon=”arrow_back” text_align=”left” background_color=”#f5f5f5″][vc_column width=”1/1″][vc_row_inner row_type=”row” type=”grid” text_align=”left” padding_top=”65″][vc_column_inner width=”2/3″][vc_separator type=”transparent” position=”center” up=”15″ down=”0″][vc_column_text]

Interprocedural Analysis

[/vc_column_text][vc_separator type=”transparent” position=”center” up=”40″ down=”0″][vc_column_text]The Goanna static analysis tool has a unique patent pending ability to efficiently analyze 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 as a parameter to a function f and later from f to a function g. It is only in g that the pointer p finally gets dereferenced.

The resulting null-pointer dereference is hard to spot by other means such as code reviews while Goanna technology automatically detects these serious issues.

Internally, the Goanna tool constructs sophisticated summaries for each function and propagates these summaries efficiently across the call graph. By enabling interprocedural analysis in Goanna, all of the new information gets included in existing checks, making them in essence more precise.[/vc_column_text][vc_separator type=”transparent” position=”center” up=”60″ down=”0″][/vc_column_inner][vc_column_inner width=”1/3″][vc_single_image image=”22292″ border_color=”grey” img_link_target=”_self” img_size=”medium” alignment=”center” css=”.vc_custom_1424845020406{padding-top: 15px !important;}”][/vc_column_inner][/vc_row_inner][/vc_column][/vc_row][vc_row row_type=”row” type=”full_width” icon_pack=”font_awesome” content_menu_fe_icon=”arrow_back” text_align=”left” padding_top=”85″ background_color=”#ffffff” use_row_as_full_screen_section=”no” padding_bottom=”65″][vc_column width=”1/1″][vc_row_inner row_type=”row” type=”grid” text_align=”left”][vc_column_inner width=”1/3″][vc_column_text]

SMT Solving

[/vc_column_text][vc_separator type=”transparent” position=”center” up=”35″ down=”0″][vc_column_text]Goanna uses automated theorem proving and decision procedures in so-called SAT Modular Theory solvers to reason more finely about C/C++ program semantics. This technology enables the Goanna engine to remove many potential false alarms automatically and sets it apart from many simpler techniques.[/vc_column_text][/vc_column_inner][vc_column_inner width=”1/3″][vc_column_text]

Taint Analysis

[/vc_column_text][vc_separator type=”transparent” position=”center” up=”35″ down=”0″][vc_column_text]Especially in the security space it is important to track the flow of information or tainted data across functions. Goanna makes use of sophisticated flow analysis taking program dependencies and control flow into account.[/vc_column_text][/vc_column_inner][vc_column_inner width=”1/3″][vc_column_text]

Pointer Analysis

[/vc_column_text][vc_separator type=”transparent” position=”center” up=”35″ down=”0″][vc_column_text]A critical aspect of C/C++ programs is the use of pointers. The Goanna engine implements novel pointer aliasing algorithms to detect memory corruptions and memory leaks. The Goanna approach goes beyond classical points-to analysis and obtains much more precise results.[/vc_column_text][/vc_column_inner][/vc_row_inner][/vc_column][/vc_row]