Formal Methods Meet Mobile Code Obfuscation

Android represents the most widespread mobile environment. This increasing diffusion is the reason why attackers are attracted to develop malware targeting this platform. Malware writers usually use code obfuscation techniques in order to evade the current antimalware detection and to generate new malware variants. These techniques make code programs harder to understand and they change the signature of the application making ineffective the signature extraction work. We propose a method based on formal methods able to identify whether a mobile application is obfuscated. In this preliminary work we identify one of the most widespread obfuscation technique: the code reordering. We test our method on a real-world dataset composed by Android trusted and ransomware samples, obtaining encouraging results.