Spyware detection using temporal logic

In recent years smartphones have become essential in daily life. A user can perform several operations through a smarthphone since they are increasingly similar to a personal computer. Furthermore, smartphones collect a large number of sensitive information. The most widespread mobile operating system is Android, this is the reason why malware writers target this platform. Malicious behaviours able to steal private information are called spyware. This paper aims to detect this kind of threat in mobile environment: we present a preliminary framework able to recognize Android spyware. It is based on model checking technique and it uses temporal logic formulae to identify malicious behaviours. We evaluate the proposed framework using a synthetic dataset obtaining a precision equal to 0.98 and a recall equal to 1.