Visible to the public How Discover a Malware Using Model Checking

TitleHow Discover a Malware Using Model Checking
Publication TypeConference Paper
Year of Publication2017
AuthorsMartinelli, Fabio, Mercaldo, Francesco, Nardone, Vittoria, Santone, Antonella
Conference NameProceedings of the 2017 ACM on Asia Conference on Computer and Communications Security
Conference LocationNew York, NY, USA
ISBN Number978-1-4503-4944-4
Keywordscomposability, defense, formal methods, Metrics, mobile, pubcrawl, Resiliency, security, Testing, Zero day attacks

Android operating system is constantly overwhelmed by new sophisticated threats and new zero-day attacks. While aggressive malware, for instance malicious behaviors able to cipher data files or lock the GUI, are not worried to circumvention users by infection (that can try to disinfect the device), there exist malware with the aim to perform malicious actions stealthy, i.e., trying to not manifest their presence to the users. This kind of malware is less recognizable, because users are not aware of their presence. In this paper we propose FormalDroid, a tool able to detect silent malicious beaviours and to localize the malicious payload in Android application. Evaluating real-world malware samples we obtain an accuracy equal to 0.94.

Citation Keymartinelli_how_2017