May 2004, 26pp.
An obfuscation is a program transformation whose aim is to make a program ``harder to understand'' so that reverse engineering of that program becomes more difficult. Two concerns about an obfuscation are whether it preserves behaviour and how much it changes efficiency.
This paper considers a fresh approach to obfuscation by considering the operations of a data-type, which we model as functional programs. Obfuscation is mainly applied to object-oriented programs and we can view an object as a data-type and methods as the operations. We consider and study a type of sets and implementation of its operations using functional lists. An imperative obfuscation --- array splitting --- is adapted and applied to the set operations. We will see that these particular obfuscations make little difference to efficiency of the operations.
Constructing obfuscations for imperative programs usually requires expensive program analysis, but our method allows us to derive functional obfuscations directly. Whilst establishing the correctness of imperative obfuscations can be a challenging task, our approach enables this to be achieved easily.
To date obfuscation has been an area largely untouched by the formal method approach to program correctness. We have begun to evaluate how a more mathematical view contributes to the study of obfuscating imperative programs.