LTL model-checking for malware detection

摘要: Nowadays, malware has become a critical security threat. Traditional anti-viruses such as signature-based techniques and code emulation insufficient easy to get around. Thus, it is important have efficient robust detectors. In [20,19], CTL model-checking for PushDown Systems (PDSs) was shown be technique detection. However, the approach of [20,19] lacks precision runs out memory in several cases. this work, we show that specifications could expressed more precise manner using LTL instead CTL. Moreover, can express malicious behaviors cannot since PDSs polynomial size while exponential, propose use Our consists of: (1) Modeling binary program PDS. This allows track program's stack (needed detection). (2) Introducing new logic (SLTPL) specify behaviors. SLTPL an extension with variables, quantifiers, predicates over stack. (3) Reducing detection problem PDSs. We reduce model checking emptiness Symbolic Buchi implemented our tool, applied detect viruses. results are encouraging.