Goanna (Software Bug Detection)


Team


NEW: Get Goanna 3.0 at http://www.redlizards.com

NEW: NIST/DHS Tool Exposition. See some of our excellent results from the SATE program.
NEW: FTSCS 2013: Formal Techniques for Safety-Critical Systems. Learn about safety critical embedded systems.

The Problem: Security and Quality Bugs

Software bugs are expensive. Today, there are over 4 million professional software developers who, at conservative estimate, spend 25% of their time testing and debugging programs. If we consider that the average loaded cost of a developer is about US$ 100,000, it makes software bugs a US$ 100 billion problem. And this does not even factor in delays, liabilities and recall costs.

The later bugs are detected in the software development process the more expensive they are and the more they delay the product launch. Embedded systems software suffers the most in this respect because it has to be developed in time with hardware, code has to be developed from scratch to meet the latest hardware (restricting the time available for testing), and should a bug get through it often entails a recall of the product.

The Solution: Goanna Source Analyser

The Goanna project is working on developing a fast, scalable and precise software solution that detects bugs and vulnerabilities automatically at development time in C/C++ source code.

Goanna combines the technologies of static analysis and model checking creating a unique solution. It analyses source code by identifying causal dependencies between program constructs, estimating all the program's behaviors, and provides up to 100% coverage. Goanna targets programming flaws such as memory corruption, buffer overruns, memory leaks, and command injections, which lead to potential system crashes or security vulnerabilities.

Automation & Technology

Key to the underlying technology of the Goanna source code analysis tool is the ability to perform a 100% automatic analysis. 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.

The team actively researches and develops in a number of core automated formal methods areas. These areas include:

  • Model Checking

    At the heart of Goanna is a CTL model checking engine, performing path-recise checks efficiently on a high-level of abstraction.

  • Static Analysis

    We use various static analysis techniques in direct combination with model checking, creating a new and efficient solution to scale our analysis to millions of lines of industrial C/C++ code. This includes a summary-based inter-procedural analysis, tainted data flow analysis, and tree-automata pattern matching.

  • Abstract interpretation

    Several abstraction techniques are used to balance speed and precision. Most notably, we use abstract interpretation to approximate value ranges for detecting buffer overflows, dangerous bit-shifting and similar defects.

Goanna's key features

  • Integration with existing development environments such as Eclipse and Visual Studio

    Unlike testing tools, Goanna can run directly within the embedded software developer's world (IDE). It can display results including trace navigation and the filtering and suppression of bugs, thereby taking much of the hassle out of running tests.

  • User-defined checks

    As well as using standard, out-of-the-box checks, the high-level check description language used by Goanna allows the tool to be adapted to a project's specific requirements.

  • Multithreading analysis

    Goanna uses patented model-checking technology to analyse every possible execution combination, including programs running in parallel. It is the only tool yet developed that does not rely on sequential heuristics. Instead it analyses race conditions, deadlocks and resource corruption automatically and within their concurrent context.

  • Embedded assembly checker

    Goanna is the only tool of its type that can deal with embedded assembly code. This is achieved using a three-step process: Examining C/assembly interface information for the entire program to ensure precise results; checking the assembly code against the interface description; and checking the assembly code itself. The result is no more black spots within the code.

  • Software metric dashboard

    Goanna's unique software metrics dashboard extracts data from the analysis and displays it in an easy-to-understand graphical form. Users can click on the graphic to drill down for more detailed information as required. The dashboard supports analysis of modules by bug type as well as comparative analysis across a release history and between modules within a release.

The Bigger Picture

The Goanna research project is a core part of the Software Systems Research Group's (SSRG) strategy of delivering high-assurance software and supporting software engineer with advanced tools to deliver better systems faster. The project has strong links with the formal methods teams in systems development, concurrency and verification.

The Goanna tool is one of the major SSRG software projects now available for worldwide use.

Key Outcomes

There are a number of key outcomes. First and foremost the Goanna source code analysis tool itself, which is now available for everyone both for academic as well as commercial use through Red Lizard Software. A range of new research results spanning the area of software engineering and formal methods have been published. Moreover, the results lead to a number of student theses as well as software patents. As of 2011 the Goanna software had several thousands registered users.

Interested?

For more information about NICTA's Goanna project, please contact:

Dr Ralf Huuck (project leader)
National ICT Australia Limited
University of NSW, Locked Bag 6016,
NSW 1466, Australia
Phone: +61 2 8306 0493
Fax: +61 2 8306 0405
Email: ralf.huuck@nicta.com.au

Selected Publications



Ralf Huuck
Formal Verification, Engineering and Business Value
Proceedings of Formal Techniques for Safety-Critical Systems (FTSCS 12) Kyoto, Japan, November 12-16, 2012. To appear in Electronic Proceedings in Theoretical Computer Science.

Paper: [PDF file]



Ansgar Fehnker, Ralf Huuck
Model Checking Driven Static Analysis for the Real World
Journal of Innovations in Systems and Software Engineering Springer-Verlag, doi:10.1007/s11334-012-0192-5, pages 1-12, August 2012.

Paper: [PDF file]



Maximilian Junker, Ralf Huuck, Ansgar Fehnker, Alexander Knapp
SMT-Based False Positive Elimination in Static Program Analysis
Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM 2012) Kyoto, Japan, November 12-16, 2012. Lecture Notes in Computer Science, Volume 7635, pages 316-331.

Paper: [PDF file]



Mark Bradley, Franck Cassez, Ansgar Fehnker, Thomas Given-Wilson, Ralf Huuck
GoannaSMT - A Static Analyzer with SMT-based Refinement
Proceedings Tools for Automatic Program AnalysiS (TAPAS 2012) Deauville, France, December 2012. Tool presenation

Paper: [PDF file]



Mark Bradley, Franck Cassez, Ansgar Fehnker, Thomas Given-Wilson, Ralf Huuck
High Performance Static Analysis for Industry
Proceedings Tools for Automatic Program AnalysiS (TAPAS 2012) Deauville, France, December 2012. Electronic Notes in Theoretical Computer Science (ENTCS), Volume 289, Pages 3-14

Paper: [PDF file]



Ralf Huuck, Ansgar Fehnker, and Rodiger Wolf
Model Checking Dataflow for Malicious Input
Proceedings of the 6th Workshop on Embedded Systems Security Taipei, Taiwan, Oct 2011. ACM, Article 4, 10 pages, ISBN: 978-1-4503-0819-9

Paper: [PDF file]



Mark Bradley, Ansgar Fehnker, Ralf Huuck, and Paul Steckler
Goanna Static Analysis at the NIST Static Analysis Tool Exposition
Report on the Third Static Analysis Tool Exposition (SATE 2010) U.S. National Institute of Standards and Technology (NIST) Special Publication (SP) 500-283, October, 2011.

Paper: [PDF file]



Mark Bradley, Ansgar Fehnker, and Ralf Huuck
Cyber security at software development time
Proceedings of the IEEE Defense Science Research Conference and Expo (DSR), 2011 Singapore, Aug 3-5 2011. IEEE, ISBN: 978-1-4244-9276-3



Andreas Vogelsang, Ansgar Fehnker, Ralf Huuck and Wolfgang Reif
Software Metrics in Static Program Analysis
12th International Conference on Formal Engineering Methods (ICFEM 2010) Lecture Notes in Computer Science, 2010, Volume 6447/2010, 485-500

Paper: [PDF file]



Ansgar Fehnker, Ralf Huuck, Sean Seefried
Counterexample Guided Path Reduction for Static Program Analysis
In the Festschrift of Correctness, Concurrency, and Compositionality for Willem-Paul de Roever, Lecture Notes in Computer Science, 2010, Volume 5930, Pages 322-341

Paper: [PDF file]



Michael Vistein, Frank Ortmeier, Wolfgang Reif, Ralf Huuck, Ansgar Fehnker
An Abstract Specification Language for Static Program Analysis
4th International Workshop on Systems Software Verification (SSV 2009) Electronic Notes in Theoretical Computer Science (ENTCS) Volume 254, Pages 181-197, October, 2009

Paper: [PDF file] Volume 254, Pages 65-83, October, 2009



Jörg Brauer, Ralf Huuck and Bastian Schlich
Interprocedural Pointer Analysis in Goanna
4th International Workshop on Systems Software Verification (SSV 2009) Electronic Notes in Theoretical Computer Science (ENTCS)

Paper: [PDF file] Volume 254, Pages 65-83, October, 2009



Ansgar Fehnker, Ralf Huuck, Sean Seefried, Michael Tapp
Fade to Grey: Tuning Static Program Analysis
3rd International Workshop on Harnessing Theories for Tool Support in Software (TTSS'09) Electronic Notes in Theoretical Computer Science (ENTCS) Volume 266, pp. 17-32 October, 2010.

Paper: [PDF file]



Ansgar Fehnker, Ralf Huuck and Sean Seefried
Incremental False Path Elimination for Static Software Analysis
ATVA '09 Proceedings of the 7th International Symposium on Automated Technology for Verification and AnalysisLecture Notes in Computer Science, 2009, Volume 5799/2009.

Paper: [PDF file]



Ansgar Fehnker, Ralf Huuck, Bastian Schlich, and Michael Tapp
Automatic Bug Detection in Microcontroller Software by Static Program Analysis
35th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM), January 24-30, 2009, Czech Republic

Paper: [PDF file]



Ansgar Fehnker, Joerg Brauer, Ralf Huuck, Sean Seefried
Goanna: Syntactic Software Model Checking
6th International Symposium on Automated Technology for Verification and Analysis (ATVA), October 20-23, 2008 Seoul, Korea.

Paper: [PDF file]



Ansgar Fehnker, Ralf Huuck, Felix Rauch, Sean Seefried
Some Assembly Required - Program Analysis of Embedded System Code
Proceedings of the Eighth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM), 28th-29th September 2008, Beijing, China

Paper: [PDF file]



Ansgar Fehnker, Ralf Huuck, Felix Rauch and Sean Seefried
Analysing Embedded System Software
Proceedings of C/C++ Verification Workshop, Oxford, UK, July, 2007

Extended Abstract: [PDF file]



Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg and Felix Rauch
Model checking software at compile time
Proceedings of the 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering, Shanghai, China, June, 2007

Paper: [PDF file]



Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg and Felix Rauch
Goanna - A Static Model Checker In the proceedings of 11th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), Bonn, Germany, August, 2006.

Paper: [PDF file]



Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco.
L4cars. In the proceedings of Embedded Security in Cars (escar 2005), Cologne, Germany, November, 2005.

Paper: [PDF file]



Gerwin Klein, Ralf Huuck
High Assurance System Software. In: Tony Cant (ed), Proc. 10th Australian Workshop on Safety Critical Systems and Software (SCS'05), Conferences in Research and Practice in Information Technology, 55, 2005.