Using Haskell to Model Tree Obfuscations

Abstract

An obfuscation is a program transformation whose aim is to make a program "harder to understand" so that reverse engineering of that program becomes difficult. Obfuscation is applied mainly to object-oriented programs.

This paper presents a fresh approach to obfuscation by considering obfuscation of objects, whose methods are modelled as functional programs. In that way we are able to obfuscate the objects knowing that it can be accessed only through the methods declared. We concentrate on an object of binary trees and find that our approach enables us to define obfuscations containing randomness designed to defeat an adversary hoping to reverse engineer the result.

To date obfuscation has been an area largely untouched by the formal method approach to program correctness. Formal methods allow us to establish a framework that provides support for the obfuscation of tree objects which exploit properties of trees. Establishing the correctness of imperative obfuscations can be a challenging task but our approach enables this to be achieved easily for all our obfuscations.