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.
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.
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.
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
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
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
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.
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
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
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
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)
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.
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.
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
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.
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
Ansgar Fehnker, Ralf Huuck, Felix Rauch and Sean Seefried Analysing Embedded System Software Proceedings of C/C++ Verification Workshop, Oxford, UK, July, 2007
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
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.
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.
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.
