Branch Obfuscation: An Efficient Binary Code Obfuscation to Impede Symbolic Execution

Symbolic execution can collect branch conditions along a concrete execution trace of a program and build a logical formula describing the program execution path. Then the logical formula is used to reason about the dependence of control flow on user inputs, network inputs and other inputs from the execution environment, which can be used to effectively direct dynamic analysis to explore execution path space of the program. Symbolic execution has been widely used in vulnerability detection, code reuse, protocol analysis and so on. But it can be also used for malicious purposes, e.g., software cracking, software tampering and software piracy. The reverse engineering based on symbolic execution is a new threat to software protection. This paper proposes a novel binary code obfuscation scheme that obfuscates branch conditions to make it difficult for symbolic execution to collect branch conditions from the execution trace. It conceals branch information by substituting conditional jump instructions with conditional exception codes and uses exception handler to transfer control. It also introduces opaque predicates into the obfuscated program to impede statistical analysis. Furthermore, this paper provides insight into the potency, resilience and cost of the branch obfuscation. Experimental result shows that branch obfuscation is able to protect various branch conditions and reduces the leakage of branch information at run-time that impedes reverse engineering based on symbolic execution to analyze programs internal logic.