ABSTRACT
With the rise of increasingly advanced reverse engineering technique, especially more scalable symbolic execution tools, software obfuscation faces great challenges. Branch conditions contain important control flow logic of a program. Adversaries can use powerful program analysis tools to collect sensitive program properties and recover a program’s internal logic, stealing intellectual properties from the original owner. In this thesis, we propose a novel control obfuscation technique that uses lambda calculus to hide the original computation semantics and makes the original program more obscure to understand and reverse engineer. Our obfuscator replaces the conditional instructions with lambda calculus expressions that simulate the same behavior with a more complicated execution model. Our experiment result shows that our obfuscation method can protect sensitive branch conditions from state-of-the-art symbolic execution techniques, with only modest overhead.
Chapter 1
INTRODUCTION
With the notable advancement of binary analysis techniques, reverse engineering is becoming more effective than ever before. As a result, malicious parties are able to employ the latest binary analysis tools to identify software vulnerabilities and exploit them to inject malicious codes into legit applications. Binary analysis tools can also get misused to reveal important internal logic of the distributed software copies, potentially leading to intellectual property thefts and therefore severe financial loss to the original developers.
One of the protection techniques that prevents undesired reverse engineering is software obfuscation. Generally, software obfuscation is the program transformation that makes software more complicated than its original form and difficult for adversaries to understand and analyze, while preserving the program’s original semantics [1] .
In this thesis, we propose a novel obfuscation method, called lambda obfuscation, which utilizes the concept of lambda calculus, a powerful formal computation system widely adopted by the programming language community. The main idea of our approach is to utilize the unique computation model of lambda calculus, which is vastly different from the widely used imperative programming paradigm, to simulate the computation of certain parts in the original programs. Instead of performing computation with data and control in imperative programming, lambda calculus is entirely based on function application and reduction. The concept of control flow becomes insignificant in lambda calculus, and all data structures, including primitive data types like integers, can be represented as high-order functions, potentially making conventional information flows implicit. With this highly abstract computation model implemented by the low-level machine code, there will be a huge semantics gap that imposes great challenges on automated program analysis and reverse engineering. Being Turing complete and considered as the smallest universal programming language [2] , lambda calculus is capable of using its reduction rules to express any kind of imperative computation. If the simulated computation is free of side effects, the source-level conversion can be quite straightforward, yet the resulting program binary after transformation will become much more complicated and obscure.
To demonstrate the value of our technique, we have implemented a prototype of the lambda obfuscation based on LLVM [3] . The obfuscator can transform qualified conditional instructions into corresponding function calls that simulate original behavior using lambda calculus. An interpreter that evaluates lambda calculus is linked to compiled binaries to return correct signals that can guide following conditional jump instructions. In such way, the behavior of conditional instructions 3
is preserved while the execution is through lambda calculus to increase the complexity. We evaluate our obfuscation technique in four aspects, namely potency, resilience, cost and stealth. The evaluation result shows that our method can make the obfuscated programs more obscure and prevent automatic software analyzers from revealing possible execution paths. In particular, we assessed lambda obfuscation’s resilience against KLEE, an advanced symbolic execution engine [4] and obtained promising results.
The rest of the thesis is organized as follows. We first discuss related work on control obfuscation in Chapter 2. We then briefly introduce the basics of lambda calculus, followed by the design of lambda obfuscation in Chapter 3. The technical details of the implementation are presented in Chapter 4. Chapter 5 presents the evaluation result of our approach. Some research questions are discussed in
Chapter 6 and we finally conclude the thesis in Chapter 7.
LAMBDA OBFUSCATION