General topic
Obfuscation; Reverse engineering; Automated Symbolic Deobfuscation
Motivation
Software deobfuscation is a crucial activity in security analysis and especially in malware analysis. While standard static and dynamic approaches suffer from well-known shortcomings, Dynamic Symbolic Execution (DSE) has recently been proposed as an interesting alternative, more robust than static analysis and more complete than dynamic analysis. Yet, DSE addresses only certain kinds of questions encountered by a reverser, namely feasibility questions (prove that a point or branch in code is reachable), while many issues arising during reverse, e.g. detecting protection schemes such as opaque predicates, fall into the category of infeasibility questions (prove that a point or branch in code is not reachable). Moreover, DSE suffers from scalability issues as it must starts from the program entry point.
Contributions
This article presents Backward-Bounded DSE, a generic, precise, efficient and robust method for solving infeasibility questions, for example identifying opaque predicates in a protected binary code. Contrary to DSE, Backward-Bounded DSE is local, thus scalable. Still it remains very precise. Especially, the technique has successfully been used on state-of-the-art packers as well as on some APT malware.
Backward-Bounded DSE does not superseed existing DSE approaches, but rather complements them by addressing infeasibility questions in a scalable and precise manner.
This work paves the way for robust, efficient and precise disassembly tools for heavily-obfuscated binaries.
Further information
- Read the paper.
- Presented at The 38st IEEE Symposium on Security and Privacy.