Abstract: |
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. |