Orion is a tool that analyzes C and C++ source code for common programming errors. Because it performs static (i.e. compile-time) analysis, it cannot be completely accurate. The messages it produces indicate potential errors - in other words, it will sometimes produce false alarms. The development of Orion is aimed at achieving a high accuracy.
Having to sift through many false alarms tends to quickly discourage use of static analysis tools. Orion subjects each potential error trace that it finds to a check to see whether it corresponds to a feasible execution path. These checks use third-party solvers that perform symbolic reasoning over the error trace. Finding an acceptable point in the trade-off between the "signal-to-noise ratio" in the error reports and the time spent in the solvers is one of the research goals behind Orion.
To achieve a high coverage, Orion re-uses the search algorithm implemented in Uno.
Orion uses the GCC compiler to parse files. Although GCC accepts a fairly broad range of C and C++ variants, some source code may have to be adapted before it is properly parsed.
A prototype version of Orion has been tested on several open source programs, among others sendmail, jpeg library, part of the linux kernel, VeriSoft, Spin, and uno.
Compared to commercially available static analyzers like FlexeLint, Orion has a more limited focus, namely on deeper, more semantic bugs such as uses of uninitialized variables and out-of-bounds array indices and pointer dereferences. In order to uncover such bugs with a higher degree of accuracy, Orion reasons symbolically about execution traces through larger segments of code, sometimes across different functions. On these tasks, Orion matches and often outperforms FlexeLint on the signal-to-noise ratio it achieves, without unacceptable increases in analysis time.
A report on Orion's application to the linux kernel is available here.
Further development of Orion, as well as its integration with the VeriSoft dynamic analysis tool, are partly funded by the joint NSF/NASA program on Highly Dependable Computing and Communication Systems Research (HDCCSR). (National Science Foundation Grant No. 0341658. Any opinions, findings, and conclusions of recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.)
The proposed project will focus on techniques and tools for high-precision static and dynamic analyses of software. Current static analyzers often suffer from a high spurious error ratio, while dynamic analysis tools generally provide only partial coverage of program executions. It will be studied how to build on techniques from program abstraction, model checking, and theorem proving, to improve this status quo. At its core, the proposal is to investigate the trade-off between the quality of the analysis results, and the computational effort needed to obtain them.The broad impact will be to enable the creation of software that is more robust, with shorter development times. In addition, it is expected that the research will lead to a better scientific understanding of several core techniques. A key component of the proposal is to build effective tools that incorporate these research results. These tools will enable the application of our research ideas to the NASA testbed, and communicate them to the programming community at large. The research results are also expected to be communicated to the research community through conference and journal publications.
More information is available here.
There are as yet no papers available on the Orion tool. For an overview of some of the research underpinning the tool, see the publications pages of Dennis Dams and Kedar Namjoshi.