Call Graph and Model Checking for Fine-Grained Android Malicious Behaviour Detection

Applied Sciences

Antonella Santone¹  Giacomo Iadarola²  Fabio Martinelli²  Francesco Mercaldo² 

[1] Department of Medicine and Health Sciences “Vincenzo Tiberio”, University of Molise, 86100 Campobassoo, Italy;Institute for Informatics and Telematics, National Research Council of Italy, 56124 Pisa, Italy;

关键词: malware;    model checking;    formal methods;    security;    Android;    mobile;   

DOI  :  10.3390/app10227975

来源: DOAJ

【 摘 要 】

The increasing diffusion of mobile devices, widely used for critical tasks such as the transmission of sensitive and private information, corresponds to an increasing need for methods to detect malicious actions that can undermine our data. As demonstrated in the literature, the signature-based approach provided by antimalware is not able to defend users from new threats. In this paper, we propose an approach based on the adoption of model checking to detect malicious families in the Android environment. We consider two different automata representing Android applications, based respectively on Control Flow Graphs and Call Graphs. The adopted graph data structure allows to detect potentially malicious behaviour and also localize the code where the malicious action happens. We experiment the effectiveness of the proposed method evaluating more than 3000 real-world Android samples (with 2552 malware belonging to 21 malicious family), by reaching an accuracy ranging from 0.97 to 1 in malicious family detection.

【 授权许可】

Unknown