Data flow analysis is a static analysis technique for calculating facts of interest at each program point, based on the control flow graph representation of the program [vJ11, p. 1254].
A canonical data flow analysis is reaching definitions analysis [NNH99, Sec. 2.1.2].
For example, if statement is x := y◻z, where ◻ is any operator, and x is defined at statement .
Reaching definitions analysis determines for each statement that uses variable x which previous statement defined x.
Example 1 [vJ11, pp. 1254-1255]
In the example below, the definition x at line 1 reaches line 2, but does not reach beyond line 3 because x is assigned on line 3.
1 x := y + z;
2 w := x + z;
3 x := w;
More formally, data flow analysis can be expressed in terms of lattice theory, where facts about a program are modelled as vertices in a lattice.
The lattice meet operator determines how two sets of facts are combined.
Given an analysis where the lattice meet operator is well-defined and the lattice is of finite height, a data flow analysis is guaranteed to terminate and converge to an answer for each statement in the program using a simple iterative algorithm.
A typical application of data flow analysis to security is to determine whether a particular program variable is derived from user input (tainted) or not (untainted).
Given an initial set of variables initialised by user input, data flow analysis can determine (typically an over approximation of) all variables in the program that are derived from user data.
