Efficient Malware Detection Using Model-Checking

摘要: Over the past decade, malware costs more than $10 billion every year and cost is still increasing. Classical signature-based emulation-based methods are becoming insufficient, since writers can easily obfuscate existing such that new variants cannot be detected by these methods. Thus, it important to have robust techniques for detection. In our previous work [24], we proposed use model-checking identify malware. We used pushdown systems (PDSs) model program (this allows keep track of program’s stack behavior), defined SCTPL logic specify malicious behaviors, where seen as an extension branching-time temporal CTL with variables, quantifiers, predicates over stack. Malware detection was then reduced PDSs. However, in way behaviors not very precise. Indeed, names registers memory locations instead their values. show this how sidestep limitation precise formulas consider values Moreover, make procedure efficient, propose abstraction reduces drastically size model, preserves all SCTPL∖X formulas, a fragment sufficient precisely characterize specifications. implemented tool applied automatically detect several malwares. The experimental results encouraging.