Welcome > Logics > FM > Abs Int

Abs Int

PPA version

Reference ¹

The theory of Abstract Interpretation is a general methodology for calculating analyses rather than just specifying them and then rely on a posteriori validation.

Collecting Semantics

records the set of traces $tr$ that can reach a given program point:

$tr \in Trace = (Var \times Lab)^*$

e.g:

$((x, ?), (y, ?), (z, ?), (y, 1), (z, 2), (z, 4), (y, 5), (z, 4), (y, 5), (y, 6))$

is the trace to run the while loop twice in the example factorial program:

$[y:=x]^1; [z:=1]^2; while [y>1]^3 do ([z:=z*y]^4; [y:=y-1]^5); [y:=0]^6$

Semantic reaching definitions.

Defined as:

$SRD(tr)(x) = l$ , iff (x,l) is the rightmost pair for $x$ in $tr$ .

can be used to test the result of the Reaching Definition Analysis. To be corrent, we should have:

$\forall x \in Var: (x, SRD(tr)(x)) \in RD_{entry}(l)$ .

Note that this only requires all correct reaching defs should be included in the result, and does not exclude false reaching defs from the result. This property is defined as ‘safe’ or ‘correct’ property of the analysis (in PPA context).

Collecting Semantics.

Collecting semantics:

a superset of the possible traces at the various program points.

For example:

$CS_{exit} (1) = \{ tr: (y,1) | tr \in CS\_entry(1) \}$

$CS_{exit} (2) = \{ tr: (z,2) | tr \in CS\_entry(2) \}$

$CS_{exit} (5) = \{ tr: (y,5) | tr \in CS\_entry(5) \}$

… total 6.

Where $tr: (x,l)$ is to append an element (x,l) to a trace $tr$ . For example, $(x_1, l_1), … , (x_n,l_n): (x,l)$ equals $(x_1, l_1), …, (x_n, l_n), (x,l).$

$CS_{entry} (3) = CS\_exit (2) \cup CS\_exit (5)$

$CS_{entry} (4) = CS\_exit (3)$

$CS_{entry} (6) = CS\_exit (3)$

… total 6.

Information about value of $y$ : make $CS{entry}(4) $and$ CS{entry} (6)$ more precise.

Rewrite the above system of equations:

$\vec{CS}$ = $G(\vec{CS})$

where $\vec{CS}$ is a 12-tuple containing the $CS$ for all 12 program points. $G$ is monotone function²:

G: $(P(Trace))^{12} \rightarrow (P(Trace))^{12}$

Solutions of the equation system: set of reaching definitions for each statement/label.

A theory: has a least solution, as $lfp(G)$

Problem: $(P(Trace))^{12}$ is not finite.

Galois Connections

Collecting semantics: operates on set of traces.

Reaching definition analysis: operates on set of pairs of variables and lables.

Use one abstract functions $\alpha$ and one concretisation function $\gamma$ to relate these two “worlds”:

$\alpha : P(Trace) \rightarrow P(Var \times Lab)$

$\gamma : P(Var \times Lab) \rightarrow P(Trace)$

$\alpha$ : extracts the reachability information present in a set of traces;

$\alpha(X) = \{(x,SRD(tr)(x)) | x \in Var \wedge tr \in X \}$

$\gamma$ , the concretisation function, produces all traces $tr$ that are consistent with the given reachability information:

$\gamma(Y) = \{ tr | \forall x \in Var: (x, SRD(tr)(x)) \in Y \}$

Often: $\alpha(X) \subseteq Y \Leftrightarrow X \subseteq \gamma(Y)$ , then $(\alpha, \gamma)$ is an adjunction, or a Galois connection.

Induced Analysis

PPA. chapter 1.5, 4. ↩
A monotone function F: $\vec{RD} \sqsubseteq \vec{RD’}$ implies $F(\vec{FD}) \sqsubseteq F(\vec{RD’})$ ↩

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?