Introduction to Software Engineering/Quality/Static Analysis

Static program analysis is the analysis of computer software that is performed without actually executing programs built from that software (analysis performed on executing programs is known as dynamic analysis). In most cases the analysis is performed on some version of the source code and in the other cases some form of the object code. The term is usually applied to the analysis performed by an automated tool, with human analysis being called program understanding, program comprehension or code review.

The sophistication of the analysis performed by tools varies from those that only consider the behavior of individual statements and declarations, to those that include the complete source code of a program in their analysis. Uses of the information obtained from the analysis vary from highlighting possible coding errors (e.g., the lint tool) to formal methods that mathematically prove properties about a given program (e.g., its behavior matches that of its specification).

It can be argued that software metrics and reverse engineering are forms of static analysis.

A growing commercial use of static analysis is in the verification of properties of software used in safety-critical computer systems and locating potentially vulnerable code. For example, medical software is increasing in sophistication and complexity, and the U.S. Food and Drug Administration (FDA) has identified the use of static code analysis as a means of improving the quality of software^[1].

Formal methods

Formal methods is the term applied to the analysis of software (and hardware) whose results are obtained purely through the use of rigorous mathematical methods. The mathematical techniques used include denotational semantics, axiomatic semantics, operational semantics, and abstract interpretation.

It has been proven that, barring some hypothesis that the state space of programs is finite, finding all possible run-time errors, or more generally any kind of violation of a specification on the final result of a program, is undecidable: there is no mechanical method that can always answer truthfully whether a given program may or may not exhibit runtime errors. This result dates from the works of Church, Kurt Gödel and Turing in the 1930s (see the halting problem and Rice's theorem). As with most^{[citation needed]} undecidable questions, one can still attempt to give useful approximate solutions.

Some of the implementation techniques of formal static analysis include:

Model checking considers systems that have finite state or may be reduced to finite state by abstraction;
Data-flow analysis is a lattice-based technique for gathering information about the possible set of values;
Abstract interpretation models the effect that every statement has on the state of an abstract machine (i.e., it 'executes' the software based on the mathematical properties of each statement and declaration). This abstract machine over-approximates the behaviours of the system: the abstract system is thus made simpler to analyze, at the expense of incompleteness (not every property true of the original system is true of the abstract system). If properly done, though, abstract interpretation is sound (every property true of the abstract system can be mapped to a true property of the original system)^[2]. The Frama-c framework and Polyspace heavily rely on abstract interpretation.
Use of assertions in program code as first suggested by Hoare logic. There is tool support for some programming languages (e.g., the SPARK programming language (a subset of Ada) and the Java Modeling Language — JML — using ESC/Java and ESC/Java2, ANSI/ISO C Specification Language for the C language).

References

↑ FDA (2010-09-08). "Infusion Pump Software Safety Research at FDA". Food and Drug Administration. Retrieved 2010-09-09.
↑ Jones, Paul (2010-02-09). "A Formal Methods-based verification approach to medical device software analysis". Embedded Systems Design. Retrieved 2010-09-09.

Bibliography

Syllabus and readings for Alex Aiken’s Stanford CS295 course.
Nathaniel Ayewah, David Hovemeyer, J. David Morgenthaler, John Penix, William Pugh, “Using Static Analysis to Find Bugs,” IEEE Software, vol. 25, no. 5, pp. 22-29, Sep./Oct. 2008, doi:10.1109/MS.2008.130
Brian Chess, Jacob West (Fortify Software) (2007). Secure Programming with Static Analysis. Addison-Wesley. ISBN 978-0321424778.
Adam Kolawa (Parasoft), Static Analysis Best Practices white paper
Improving Software Security with Precise Static and Runtime Analysis, Benjamin Livshits, section 7.3 “Static Techniques for Security,” Stanford doctoral thesis, 2006.
Flemming Nielson, Hanne R. Nielson, Chris Hankin (1999, corrected 2004). Principles of Program Analysis. Springer. ISBN 978-3540654100. {{cite book}}: Check date values in: |year= (help)CS1 maint: multiple names: authors list (link)
“Abstract interpretation and static analysis,” International Winter School on Semantics and Applications 2003, by David A. Schmidt

External links

The SAMATE Project, a resource for Automated Static Analysis tools
Integrate static analysis into a software development process
Code Quality Improvement - Coding standards conformance checking (DDJ)
Episode 59: Static Code Analysis Interview (Podcast) at Software Engineering Radio
Implementing Automated Governance for Coding Standards Explains why and how to integrate static code analysis into the build process

[1] FDA (2010-09-08). "Infusion Pump Software Safety Research at FDA". Food and Drug Administration. Retrieved 2010-09-09.

[2] Jones, Paul (2010-02-09). "A Formal Methods-based verification approach to medical device software analysis". Embedded Systems Design. Retrieved 2010-09-09.

[1]

[2]