Thwarting Themida: Unpacking Malware with SMT Solvers


Malware analysis is one of the key problems in the realm of cybersecurity. Contemporary malware is nearly always protected from examination with the use of a "packer," a program designed to obscure its malicious functionality. In the past, packers used techniques such as compression, encryption or time locks to thwart analysis.

Currently, the most advanced technique use by packers is code virtualization. In this technique, the packing software includes a virtual processor within the binary. Sections of the binary are translated to a bytecode that is read and executed by this processor. The exact operation being performed in the virtualizer is frequently obfuscated. In addition to this basic virtualization, other translations to the original code are made, for example, stealing portions of the initial code of API functions and obfuscating them within the caller.

In an attempt to counter the advantage that code virtualization gives to malware authors, CyberPoint has targeted Themida, a commercial, virtualizing packer for our work. We have developed techniques to symbolically execute portions of Themida's virtual processor, generating constraints. We can then use an SMT solver to prove properties, letting us, in many cases, undo the obfuscation and diagnose functionality. Our technique makes use of the SBV Haskell library to model the execution and interface with the new CVC4 solver.

In this talk we will discuss our techniques, their successes and further challenges that face us as we proceed in the area of advanced malware unpacking.

Ian Blumenfeld
Roberta Faux
Paul Li
Creative Commons 2.5

Other available formats:

Thwarting Themida: Unpacking Malware with SMT Solvers
Switch to experimental viewer