Static program analysis

Static program analysis

Static program analysis (also Static code analysis or SCA) 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)[1] 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. In fact deriving software metrics and static analysis are increasingly deployed together, especially in creation of embedded systems, by defining so called software quality objectives[2].

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[3]. For example the following industries have identified the use of static code analysis as a means of improving the quality of increasingly sophisticated and complex software:

  1. Medical software: In the U.S. Food and Drug Administration (FDA) has identified the use of static analysis for medical devices.[4]
  2. Nuclear software: In the UK the Health and Safety Executive recommends the use of Static Analysis on Reactor Protection Systems.[5]


In application security industry also Static Application Security Testing (SAST) name is used.

Contents

Tools

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.

By a straightforward reduction to the halting problem it is possible to prove that (for any Turing complete language) finding all possible run-time errors in an arbitrary program (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, 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).[6] 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).

See also

References

  1. ^ Industrial Perspective on Static Analysis. Software Engineering Journal Mar. 1995: 69-75Wichmann, B. A., A. A. Canning, D. L. Clutterbuck, L. A. Winsbarrow, N. J. Ward, and D. W. R. Marsh. http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf
  2. ^ Software Quality Objectives for Source Code. Proceedings Embedded Real Time Software and Systems 2010 Conference, ERTS2, Toulouse, France: Patrick Briand, Martin Brochet, Thierry Cambois, Emmanuel Coutenceau, Olivier Guetta, Daniel Mainberte, Frederic Mondot, Patrick Munier, Loic Noury, Philippe Spozio, Frederic Retailleau http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0035_final.pdf
  3. ^ Improving Software Security with Precise Static and Runtime Analysis, Benjamin Livshits, section 7.3 “Static Techniques for Security,” Stanford doctoral thesis, 2006. http://research.microsoft.com/en-us/um/people/livshits/papers/pdf/thesis.pdf
  4. ^ FDA (2010-09-08). "Infusion Pump Software Safety Research at FDA". Food and Drug Administration. http://www.fda.gov/MedicalDevices/ProductsandMedicalProcedures/GeneralHospitalDevicesandSupplies/InfusionPumps/ucm202511.htm. Retrieved 2010-09-09. 
  5. ^ Computer based safety systems - technical guidance for assessing software aspects of digital computer based protection systems, http://www.hse.gov.uk/foi/internalops/nsd/tech_asst_guides/tast046app1.htm
  6. ^ Jones, Paul (2010-02-09). "A Formal Methods-based verification approach to medical device software analysis". Embedded Systems Design. http://embeddeddsp.embedded.com/design/opensource/222700533. Retrieved 2010-09-09. 

Bibliography

External links


Wikimedia Foundation. 2010.

Игры ⚽ Нужно сделать НИР?

Look at other dictionaries:

  • Static code 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… …   Wikipedia

  • Program analysis (computer science) — Computer program analysis is the process of automatically analysing the behavior of computerprograms.Two main approaches in program analysis are static program analysisand dynamic program analysis.Main applications of program analysis are program …   Wikipedia

  • Program analysis — For other uses, see Program analysis (disambiguation). In computer science, program analysis is the process of automatically analysing the behavior of computer programs. Two main approaches in program analysis are static program analysis and… …   Wikipedia

  • List of tools for static code analysis — This is a list of significant tools for static code analysis.Historical products* Lint the original static code analyzer of C code.Open source or Noncommercial products .NET (C#, VB.NET and all .NET compatible languages) *… …   Wikipedia

  • Dynamic program analysis — is the analysis of computer software that is performed by executing programs built from that software system on a real or virtual processor. For dynamic program analysis to be effective, the target program must be executed with sufficient test… …   Wikipedia

  • Analysis — (from Greek ἀνάλυσις , a breaking up ) is the process of breaking a complex topic or substance into smaller parts to gain a better understanding of it. The technique has been applied in the study of mathematics and logic since before Aristotle,… …   Wikipedia

  • Program slicing — In computer programming, program slicing is the computation of a program slice. The program slice consists of the parts of a program that may affect the values computed at some point of interest, referred as a slicing criterion. Program slicing… …   Wikipedia

  • Termination analysis — In computer science, a termination analysis is program analysis which attempts to determine whether the evaluation of a given program will definitely terminate. Because the halting problem is undecidable, termination analysis cannot work… …   Wikipedia

  • Dependence analysis — In compiler theory, dependence analysis produces execution order constraints between statements/instructions. Broadly speaking, a statement S2 depends on S1 if S1 must be executed before S2. Broadly, there are two classes of dependencies control… …   Wikipedia

  • Static single assignment form — In compiler design, static single assignment form (often abbreviated as SSA form or SSA) is an intermediate representation (IR) in which every variable is assigned exactly once. Existing variables in the original IR are split into versions , new… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”