Malware Analysis through Behavior Formalization

Malware analysis represents a difficult task due to its ever-changing nature, where attackers invent new techniques for avoiding or counter-attacking analysis and prevention mechanisms. During fast-response investigations, a vital element is extracting or checking information, in order to take proper action. One key aspect that is currently missing, in a general sense, is a system which security researchers can query in order to obtain a quick verdict about the capabilities of a malware. The proposed solution is a framework for formal analysis of applications’ behavior, called Formal Tainting-Based Framework, that uses a combination of binary instrumentation, taint analysis, and runtime verification in order to selectively extract behavioral properties of a malware. These are then formalized in order to check if the application expresses certain capabilities. The formal aspect also represents a significant contribution, as we introduce a specific temporal logic, which overcomes obstacles for expressing program events. The findings are accompanied by a concrete implementation, which proved effective and efficient against real-life malware, as highlighted by an evaluation. Furthermore, the framework has been evaluated in realistic cyber forensics scenarios, demonstrating its potential to assist security researchers by reducing analysis time and effort.