Reference 1
The theory of Abstract Interpretation is a general methodology for calculating analyses rather than just specifying them and then rely on a posteriori validation.
records the set of traces tr that can reach a given program point:
tr∈Trace=(Var×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]3do([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:
∀x∈Var:(x,SRD(tr)(x))∈RDentry(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:
CSexit(1)={tr:(y,1)|tr∈CS_entry(1)}
CSexit(2)={tr:(z,2)|tr∈CS_entry(2)}
CSexit(5)={tr:(y,5)|tr∈CS_entry(5)}
… total 6.
Where tr:(x,l) is to append an element (x,l) to a trace tr. For example, (x1,l1),…,(xn,ln):(x,l) equals (x1,l1),…,(xn,ln),(x,l).
CSentry(3)=CS_exit(2)∪CS_exit(5)
CSentry(4)=CS_exit(3)
CSentry(6)=CS_exit(3)
… total 6.
Information about value of y: make $CS{entry}(4)andCS{entry} (6)$ more precise.
Rewrite the above system of equations:
→CS = G(→CS)
where →CS is a 12-tuple containing the CS for all 12 program points. G is monotone function2:
G: (P(Trace))12→(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.
Collecting semantics: operates on set of traces.
Reaching definition analysis: operates on set of pairs of variables and lables.
Use one abstract functions α and one concretisation function γ to relate these two “worlds”:
α:P(Trace)→P(Var×Lab)
γ:P(Var×Lab)→P(Trace)
α: extracts the reachability information present in a set of traces;
α(X)={(x,SRD(tr)(x))|x∈Var∧tr∈X}
γ, the concretisation function, produces all traces tr that are consistent with the given reachability information:
γ(Y)={tr|∀x∈Var:(x,SRD(tr)(x))∈Y}
Often: α(X)⊆Y⇔X⊆γ(Y), then (α,γ) is an adjunction, or a Galois connection.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?