Reverse Engineering Stack Exchange is a question and answer site for researchers and developers who explore the principles of a system through analysis of its structure, function, and operation. It only takes a minute to sign up.
Sign up to join this community
I was reading through the chapter on Obfuscation in "Practical Reverse Engineering" I encountered the following statement.
Where X is the set of execution traces (finite and infinite), you can express the trace semantics as the least solution (for the computational partial ordering) of a fixpoint equation X = F( X).
Could someone explain what that means in simple terms? If you could point me towards any resources for further reading and learning, that'd be great too.
You may consult pages 39-41 in the thesis
"Code Obfuscation and Malware Detection by Abstract Interpretation"
of M. Dalla Preda about formal obfuscation; or sections 4.4 and 4.5 in the orignal paper
"Systematic Design of Program Transformation Frameworks by Abstract Interpretation"
of Cousot and Cousot.
The theory is formal and requires much more technical details than the following interpretation, but the idea is that:
The "finite trace" semantics of a program P is defined by the set of all finite traces of P. A trace is nothing but a finite sequence of states of P, obtained when running P, step-by-step over "commands" of P.
(You may note that, from a state, we can get a set of possible next states, because the command at this state can be nondeterministic: it can receive some value from environment).
To calculate the finite trace semantics of P, one way (which one is refered in your book) is to use a function F defined from FinSeqs to FinSeqs:
F : FinSeq -> FinSeq
where FinSeqs is the set of all "sub-set of finite sequences of states of P" (you may think that each sub-set is a possible value for the "finite trace" semantics of P).
This function F map a sub-set X to a sub-set X' so that each trace x' of X' has a trace x of X as suffix (that is the reason why it is called "backward" in the paper of Cousot and Cousot). Particularly, we have that
x' = sj . x
x = si . x1
and sj must be able to be a next state of si. The least fixpoint of the function F, namely some set Xp so that
F(Xp) = Xp
is called the trace semantics of P.
