Model checking for malicious family detection and phylogenetic analysis in mobile environment

Malware targeting mobile devices is widespread, in fact considering the great amount of sensitive and private information stored in tablets and smartphones they represent an interesting surface attack for malware developers. From the defensive side, the well-known weaknesses of the current anti-malware technologies do not permit only the detection of new obfuscated malicious payloads, but also of obfuscated malware (even with trivial obfuscation techniques applied with automatic morphing engines). In fact, a threat is recognized only if its signature is present in the anti-malware repository and typically the signature extraction consists in a time consuming task performed by security analysts. In this paper we propose a two-fold method aimed to (i) detect the belonging family of a mobile malicious application and (ii) collocate the application in the right position in the phylogenetic tree. We represent application system call traces in terms of automaton and, through the adoption of process mining, we extract temporal logic property verified with the adoption of a formal verification environment. The evaluation on a data-set composed by more than 12,000 Android applications (4552 malicious ranging from 2010 to 2018, 4552 obfuscated with three different obfuscation engines and 3500 legitimate) confirms the effectiveness of the proposed formal methods-based approach, obtaining an accuracy ranging from 0.882 to 0.987 in the analysis of 12 real-world widespread malicious families implementing different behaviours.