Static code analysis - AbsoluteAstronomy.com

Static program analysis (also Static code analysis or SCA) is the analysis of computer software

Program analysis (computer science)

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 dynamic program analysis...

that is performed without actually executing programs built from that software (analysis performed on executing programs is known as dynamic analysis

Dynamic program analysis

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 inputs to produce interesting...

) In most cases the analysis is performed on some version of the source code

Source code

In computer science, source code is text written using the format and syntax of the programming language that it is being written in. Such a language is specially designed to facilitate the work of computer programmers, who specify the actions to be performed by a computer mostly by writing source...

and in the other cases some form of the object code

Object code

Object code, or sometimes object module, is what a computer compiler produces. In a general sense object code is a sequence of statements in a computer language, usually a machine code language....

. The term is usually applied to the analysis performed by an automated tool, with human analysis being called program understanding, program comprehension

Program comprehension

Program comprehension is a domain of computer science concerned with the ways software engineers maintain existing source code. The cognitive and other processes involved are identified and studied...

or code review

Code review

Code review is systematic examination of computer source code. It is intended to find and fix mistakes overlooked in the initial development phase, improving both the overall quality of software and the developers' skills...

.

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

Lint programming tool

In computer programming, lint was the name originally given to a particular program that flagged some suspicious and non-portable constructs in C language source code. The term is now applied generically to tools that flag suspicious usage in software written in any computer language...

tool) to formal methods

Formal methods

In computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...

that mathematically prove properties about a given program (e.g., its behavior matches that of its specification).

It can be argued that software metric

Software metric

A software metric is a measure of some property of a piece of software or its specifications. Since quantitative measurements are essential in all sciences, there is a continuous effort by computer science practitioners and theoreticians to bring similar approaches to software development...

s and reverse engineering

Reverse engineering

Reverse engineering is the process of discovering the technological principles of a device, object, or system through analysis of its structure, function, and operation...

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.

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

Vulnerability (computing)

In computer security, a vulnerability is a weakness which allows an attacker to reduce a system's information assurance.Vulnerability is the intersection of three elements: a system susceptibility or flaw, attacker access to the flaw, and attacker capability to exploit the flaw...

code. 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:

Medical software
Medical software
In computers, medical software is a significant branch of software engineering. Many medical devices that monitor or control patients are predominantly controlled by software. Medical devices are frequently regulated and must comply with local and regional laws. In the European Union, these...

: In the U.S. Food and Drug Administration
Food and Drug Administration
The Food and Drug Administration is an agency of the United States Department of Health and Human Services, one of the United States federal executive departments...

(FDA) has identified the use of static analysis for medical devices.
Nuclear software: In the UK the Health and Safety Executive
Health and Safety Executive
The Health and Safety Executive is a non-departmental public body in the United Kingdom. It is the body responsible for the encouragement, regulation and enforcement of workplace health, safety and welfare, and for research into occupational risks in England and Wales and Scotland...

recommends the use of Static Analysis on Reactor Protection Systems
Reactor Protective System
A reactor protection system is a set of nuclear safety components in a nuclear power plant designed to safely shutdown the reactor and prevent the release of radioactive materials. The System can "trip" automatically , or it can be tripped by the operators. Trips occurs when the parameters meet...

.

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

Formal methods

Formal methods is the term applied to the analysis of software (and hardware

Hardware

Hardware is a general term for equipment such as keys, locks, hinges, latches, handles, wire, chains, plumbing supplies, tools, utensils, cutlery and machine parts. Household hardware is typically sold in hardware stores....

) whose results are obtained purely through the use of rigorous mathematical methods. The mathematical techniques used include denotational semantics

Denotational semantics

In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...

, axiomatic semantics

Axiomatic semantics

Axiomatic semantics is an approach based on mathematical logic to proving the correctness of computer programs. It is closely related to Hoare logic....

, operational semantics

Operational semantics

In computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Operational semantics are classified into two categories: structural operational semantics formally describe how the individual steps of a computation take place in a...

, and abstract interpretation

Abstract interpretation

In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics In...

.

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

Decision problem

In computability theory and computational complexity theory, a decision problem is a question in some formal system with a yes-or-no answer, depending on the values of some input parameters. For example, the problem "given two numbers x and y, does x evenly divide y?" is a decision problem...

: 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

Alonzo Church

Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.-Life:Alonzo Church...

, Gödel

Kurt Gödel

Kurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...

and Turing

Alan Turing

Alan Mathison Turing, OBE, FRS , was an English mathematician, logician, cryptanalyst, and computer scientist. He was highly influential in the development of computer science, providing a formalisation of the concepts of "algorithm" and "computation" with the Turing machine, which played a...

in the 1930s (see the halting problem

Halting problem

In computability theory, the halting problem can be stated as follows: Given a description of a computer program, decide whether the program finishes running or continues to run forever...

and Rice's theorem

Rice's theorem

In computability theory, Rice's theorem states that, for any non-trivial property of partial functions, there is no general and effective method to decide whether an algorithm computes a partial function with that property...

). As with most undecidable questions, one can still attempt to give useful approximate solutions.

Some of the implementation techniques of formal static analysis include:

Model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....

considers systems that have finite state or may be reduced to finite state by abstraction
Abstraction (computer science)
In computer science, abstraction is the process by which data and programs are defined with a representation similar to its pictorial meaning as rooted in the more complex realm of human life and language with their higher need of summarization and categorization , while hiding away the...

;
Data-flow analysis is a lattice-based technique for gathering information about the possible set of values;
Abstract interpretation
Abstract interpretation
In computer science, abstract interpretation is a theory of sound approximation of the semantics of computer programs, based on monotonic functions over ordered sets, especially lattices. It can be viewed as a partial execution of a computer program which gains information about its semantics In...

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). The Frama-c
Frama-C
Frama-C stands for Framework for Modular Analysis of C programs. Frama-C is a set of interoperable program analyzers for C programs. Frama-C has been developed by Commissariat à l'Énergie Atomique et aux Énergies Alternatives and Inria...

value analysis plugin and Polyspace
Polyspace
Polyspace is a static code analysis tool inspired by the failure of the maiden flight of Ariane 5 where a run time error resulted in destruction of the launch vehicle. It is the first example of large-scale static code analysis by abstract interpretation to detect and prove the absence of certain...

heavily rely on abstract interpretation.
Use of assertion
Assertion (computing)
In computer programming, an assertion is a predicate placed in a program to indicate that the developer thinks that the predicate is always true at that place.For example, the following code contains two assertions:...

s in program code as first suggested by Hoare logic
Hoare logic
Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers...

. There is tool support for some programming languages (e.g., the SPARK programming language
SPARK programming language
SPARK is a formally-defined computer programming language based on the Ada programming language, intended to be secure and to support the development of high integrity software used in applications and systems where predictable and highly reliable operation is essential either for reasons of safety...

(a subset of Ada
Ada (programming language)
Ada is a structured, statically typed, imperative, wide-spectrum, and object-oriented high-level computer programming language, extended from Pascal and other languages...

) and the Java Modeling Language
Java Modeling Language
The Java Modeling Language is a specification language for Java programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm...

— JML — using ESC/Java
ESC/Java
ESC/Java , the "Extended Static Checker for Java," is a programming tool that attempts to find common run-time errors in Java programs at compile time...

and ESC/Java2, Frama-c
Frama-C
Frama-C stands for Framework for Modular Analysis of C programs. Frama-C is a set of interoperable program analyzers for C programs. Frama-C has been developed by Commissariat à l'Énergie Atomique et aux Énergies Alternatives and Inria...

WP (weakest precondition) plugin for the C language extended with ACSL (ANSI/ISO C Specification Language
ANSI/ISO C Specification Language
The ANSI/ISO C Specification Language is a specification language for C programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm...

) ).

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
Podcast
A podcast is a series of digital media files that are released episodically and often downloaded through web syndication...

) at Software Engineering Radio
Implementing Automated Governance for Coding Standards Explains why and how to integrate static code analysis into the build process
What is Static Code Analysis? explanation in Hebrew
.NET Static Analysis (InfoQ)

The source of this article is wikipedia, the free encyclopedia. The text of this article is licensed under the GFDL.

Formal methods

See also

External links