In the most comprehensive study on Android attacks so far (undertaken by the Android Malware Genome Project), the behaviour of more than 1, 200 malwares was analysed and categorised into common, recurring groups of attacks. Based on this work (and the corresponding actual malware files), we present an approach for specifying and identifying these (and similar) attacks using runtime verification. rmally, our approach is based on a first-order logic abstraction of malware behaviour, it practically relies on our Android event interception tool, MonitorMe, which lets us capture almost any system event that can be triggered by apps on a user’s Android device. This paper details on MonitorMe, our formal specification of malware behaviour and practical experiments, undertaken with various different Android devices and versions on a wide range of actual malware incarnations from the above study. In a nutshell, we were able to detect real malwares from 46 out of 49 different malware fam...