Toward Semantic-Based Android Malware Detection Using Model Checking and Machine Learning

The ever-increasing presence of Android malware is accompanied by a deep concern about security issues in the mobile ecosystem. Android malware detection has received much attention in the research community. In fact, malware proliferation goes hand in hand with its sophistication and complexity. For instance, more elaborated malware, such as polymorphic or metamorphic malware, uses code obfuscation techniques to build new variants that preserve the semantics of the original code but modify its syntax and thus escape the usual detection methods. In the present work, we propose a model checking based approach that combines static analysis and machine learning. Mainly, from a given Android application we extract an abstract model expressed in terms of LNT, a process algebra language. This model is then checked against security related Android behaviors specified by modal \(\mu \)-calculus formulae. The satisfaction of a specific formula is considered as a feature. Finally, machine learning algorithms are used to classify the application as malicious or not. The use of temporal properties improves the classification performance.