Formal Methods for Malware Detection

Our objective is to develop highly automatic and scalable formal methods for malware detection. Existing tools for malware detection operate by searching for pattern matches with respect to signatures of known malware, and can account for only limited variations in the malware. That makes these detectors generally incapable of identifying newly released malware. Furthermore, due to the short signatures used for most malware, and the inability of these detectors to account for many code obfuscations, i.e., code transformations that preserve the malicious behavior and produce code with a radically different structure, such malware detectors are virtually incapable of identifying most of the obfuscated variants of known malware. In this proposed research we will: 1) investigate formal methods for detection of malicious intent in binary code; 2) develop automatic formal techniques to detect obfuscations that are based on reordering of the memory accesses in known malware; 3) explore formal approaches to account for obfuscations that are based on replacing instructions with different instructions that have equivalent semantics; and 4) develop efficient translations to SAT of the Boolean formulas generated in formal detection of malware in order to enable our malware detection tool to run on commodity PCs with limited memory.