Symbolic Execution of Obfuscated Codex
Babak Yadegari
Saumya Debray
Department of Computer Science
University of Arizona
Tucson, AZ 85721, U.S.A.
Abstract
Symbolic and concolic execution find important applications in a number
of security-related program analyses, including analysis of malicious code.
However, malicious code tend to very often be obfuscated, and current
concolic analysis techniques have trouble dealing with some of these
obfuscations, leading to imprecision and/or excessive resource usage.
This paper discusses three such obfuscations: two of these are already
found in obfuscation tools used by malware, while the third is a simple
variation on an existing obfuscation technique. We show empirically
that existing symbolic analyses are not robust against such obfuscations,
and propose ways in which the problems can be mitigated using a combination
of fine-grained bit-level taint analysis and architecture-aware constraint
generations. Experimental results indicate that our approach is effective
in allowing symbolic and concolic execution to handle such obfuscations.