Program obfuscation transforms source code into a complex, harder-to-analyze form while preserving functionality, commonly used for intellectual property protection and security. Although it is also exploited by malware developers. Opaque predicate obfuscation increases program size by inserting junk code with conditional expressions that prevent execution. Existing deobfuscation methods rely on symbolic execution and SMT solvers but face limitations based on predicate types. This paper proposes a logic-based deobfuscation technique capable of handling Mixed Boolean Arithmetic obfuscation and dynamic opaque predicates using I/O analysis, program synthesis, and recursive matching. Experimental results show that the proposed method outperforms existing tools against obfuscation by Code Virtualizer, Tigress, and OLLVM.

Obfuscation is a powerful software protection technique. It changes a program into a more complicated one while preserving its semantics. Malware distributors also employ this method, to protect their malware from being understood by malware analysts. Thus, it is crucial to deobfuscate malware in a timely manner, to enable a prompt action to malware.

As program obfuscation techniques have improved, attackers have incorporated obfuscation into their malware and used it to thwart malware analysis. Opaque predicate is one of the widely used obfuscation methods to thwart code analysis, and we found that dynamic opaque predicate in particular cannot be deobfuscated with existing deobfuscators. This work proposes a dynamic opaque predicate detection technique based on recursive propagating of symbolic execution.