Abstract:
An obfuscation aims to transform a program, without affecting the functionality,
so that some secret information within the program can be hidden for as long
as possible from an adversary. Proving that an obfuscating transform is correct
(i.e. it preserves functionality) is considered to be a challenging task. We use data
refinement to specify data obfuscations, model our operations using the functional
language Haskell and consider obfuscating abstract data-types. This approach
allows us to prove properties, including correctness, of our operations easily.
In this paper our focus is on how to obfuscate a data-type of binary trees for
which we specify a set of operations and a list of properties that these operations
satisfy. We consider different tree transformations and discuss their suitability as
obfuscations. In particular we show what our tree operations would be like under
these different transformations. We also discuss various ways of defining obfuscated
operations including the use of folds and unfolds and how we can exploit properties
of Haskell to add extra confusion in our obfuscated definitions.