Localization and Inhibition of Malicious Behaviors through a Model Checking based methodology

Mobile malware is increasing more and more in complexity; current signature based antimalware mechanisms are not able to detect attacks, since trivial code transformations may evade detection. Furthermore, antimalware, when correctly label an application as malicious, are able to quarantine or delete the application, but not to allow the user to install and safely use it. Here we present a model checking based approach to locate and inhibit malicious behaviors: we suppose the specification of programs in terms of process algebra language LOTOS, malicious behaviors specified by temporal logic formulae, and define a method to retrieve, from the specifications, the description of the infected part of the program. We refer as example to some Android malware and derive LOTOS specification automatically from the Java Bytecode corresponding to Android's app. The method consists of a set of rules building the LOTOS processes mirroring the behavior of the malware possibly contained in the app; besides the description of the infected part of the code, we give also a way to block the malware attack, putting the basis to disinfect the application. The method can be applied at any level of complexity, so allowing the precise location of malicious behaviors.