Download Malware? No, Thanks. How Formal Methods Can Block Update Attacks

In mobile malware landscape there are many techniques to inject malicious payload in a trusted application: one of the most common is represented by the so-called update attack. After an apparently innocuous application is installed on the victim’s device, the user is asked to update the application, and a malicious behavior is added to the application. In this paper we propose a static method based on model checking able to identify this kind of attack. In addiction, our method is able to localize the malicious payload at methodlevel. We obtain an accuracy very close to 1 in identifying families implementing update attack using a real Android dataset composed by 2,581 samples.