Assessing software robustness became arduous given the broad adoption of obfuscation in the industry and especially in mobile applications and embedded systems. As such, deobfuscation is becoming crucially important. Obfuscation usually concerns either target the control-flow or the data-flow of the program. While standard static and dynamic analyses suffer some shortcomings, Dynamic Symbolic Execution (DSE) turns out to be very effective on control-flow obfuscation. Yet, fewer approaches address issues raised by data-flow obfuscation. Program synthesis appears to be a promising approach to target such obfuscation. We present a generic approach leveraging both DSE and program synthesis to successfully synthesize programs obfuscated with Mixed-Boolean-Arithmetic, Data-Encoding or Virtualization. The synthesis algorithm proposed is an offline enumerate synthesis primitive guided by top-down breath-first search. We shows its effectiveness against a state-of-the-art obfuscator and its scalability as it supersedes other similar approaches based on synthesis. We also show its effectiveness in presence of composite obfuscation (combination of various techniques). This ongoing work enlightens the effectiveness of synthesis to target certain kinds of obfuscations and opens the way to more robust algorithms and simplification strategies.
PDF version of the paper.