Thwarting Themida: Unpacking Malware with SMT Solvers

Presented as part of the 2013 HCSS conference.

ABSTRACT

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.