Sandboxing and reasoning on malware infection trees

Malware infection trees are computational structures for analyzing and identifying different processes and files during the execution of malware. In this paper, we describe a sandboxing-based formalization to predict malware behaviors such as the possibility of file and process creation. Model checking is used as a querying mechanism on a labeled transition system representing a malware infection tree. We evaluate computational feasibility of our formalism using a case study on Backdoor.WIN32.Poison malware and behavior specified by malware infection trees.