Formal obfuscation

Question

My question is related to this question with the excellent answer of @Rolf Rolles. Since the paper of M.D. Preda et al is quite technique so I wonder whether I understand their idea or not. The following phrase is quoted from the paper:

The basic idea is to model attackers as abstract interpretations of the concrete program behaviour, i.e., the concrete program semantics. In this framework, an attacker is able to break an opaque predicate when the abstract detection of the opaque predicate is equivalent to its concrete detection.

As fas as I understand, they have given a formal model of attacker as someone trying to obtain the properties of program using a sound approximation as abstract interpretation (AI). The attacker will success if the AI procedure is complete (informally speaking, the fixed-point obtained in the abstract domain "maps" also back to the fixed-point in the concrete domain).

Concretely speaking, their model can be considered as an AI-based algorithm resolving the opaque predicate. In fact, this idea spreads everywhere (e.g. in this paper, the authors have proven that the DPLL algorithm used in SMT solvers is also a kind of abstract interpretation).

Obviously, in the worst case where the abstract interpretation is not complete then the attacker may never recover the needed properties (e.g. he can approximate but he will never recover the exact solution for a well-designed opaque predicate).

So I wonder that the model of attacker as abstract domains may have some limits, because we still not sure that all attacks can be modelled in AI. Then a straitghtforward question comes to me is "What happens if the attacker uses some other methods to resolve the opaque predicate ?."

For a trivial example, the attacker can simply use the dynamic analysis to bypass the opaque predicate (he accepts some incorrectness, but finally he may be able to get the properties he wants).

Would anyone please give me some suggestions ?

Answer 1

Any obfuscation technique (or its formalization) targets one or more assumptions made by some class of analyses A -- in essence, the obfuscation transforms a program P0 into a different representation P1 that has the same execution behavior as P0 but which violates the assumptions made by the analyses A. In doing so, the obfuscation necessarily defines a class of attacks that it is effective against; it says nothing about attacks that don't fall within that class.

Abstract interpretation is a formalization of program analysis that assumes sound static analysis (e.g., consider the requirements imposed on the abstract domain and abstraction/concretization functions). So abstract interpretation serves to formalize obfuscations that make those assumptions and helps us reason about analyses/attacks that meet those assumptions. It doesn't describe all possible obfuscations --- e.g., any obfuscation that relies on runtime code generation or modification --- and doesn't speak to attacks that don't meet those assumptions. Thus, as you propose, an attacker who uses dynamic analysis or potentially unsound techniques essentially side-steps the rules assumed by abstract interpretation.

Answer 2

If I understood it correct, you have actually answered your question yourself:

...the attacker can simply use the dynamic analysis to bypass the opaque predicate (he accepts some incorrectness, but finally he can get the properties he wants).

Opaque predicates, anti-debugging techniques, anti-reversing techniques and other protection mechanism are designed to make reversing harder, but never impossible. At times it is less important how exactly something was designed, then what it actually does. Sometimes good reverser gets to know code and design much better then people who designed it, which allows for attacks to be implemented, or patches to be created.