Characterizing Symbolic Execution Behavior on Evasive Malware

Malware analysis is a rapidly growing component of cybersecurity, driven in part by the emergence of evasive malware. The complex methods utilized in modern malicious code, such as obfuscation, environmental checking, and runtimedependent behavior, hinder static and dynamic analysis. Symbolic execution approaches can theoretically explore all execution paths to locate malicious behavior. However, evasive techniques used by malicious binaries stress the solver, leading to timeouts, incomplete exploration, and the missed detection of key structures. This work introduces SymExE, a symbolic-executionbased framework designed to provide insight into the execution behavior of evasive malware. We conduct the first empirical study of symbolic execution on real evasive malware samples, using key metrics such as code coverage, constraint complexity, and state growth across five sample size groups. Results show no strong relationship between binary size and solver strain, indicating internal code structure and evasive logic are the dominant causes of symbolic execution difficulty. Our findings provide new insight into the limitations of symbolic execution for evasive malware and highlight the importance of considering structural complexity. We further demonstrate that solver progress metrics, such as the number of states explored and the time spent, are unreliable indicators of analysis depth in evasive samples. Our approach establishes a new foundation for understanding symbolic execution of evasive malware, enabling more targeted improvements in solver design and malware analysis methodologies.