Detection of Android Malware using Model Checking and Machine Learning

Organisation:	Laval University, Québec, CANADA
Method:	LNT MCL
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Security.
Period:	2020
Size:	Android applications of 2 Mbytes
Description:	The ever-increasing presence of Android malware is accompanied by a deep concern about security issues in the mobile ecosystem. The proliferation of Android malware increases with its sophistication and complexity. 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. This work proposes a malware detection approach based on model checking combined with static analysis and machine learning. From a given Android application, an abstract model in LNT is extracted. This model is then checked against security related Android properties (virtualization by elusive applications, blocking of incoming SMSs, ransomware and spyware, usage of native code, presence of obfuscated code, checking IP addresses, DNS lookups) specified as MCL formulas. 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. It is shown that the use of temporal properties as features for the classifier enables to detect 95% of malicious Android applications.
Conclusions:	The use of formal models and model checking techniques is an important phase in the malware detection process proposed. The LNT encoding can be further extended to capture additional synchronization mechanisms (e.g., barriers) so as to improve the precision of the classifier. Also, the set of MCL formulas can be extended to characterize other suspicious behaviours, thus improving the prediction performance.
Publications:	[ElHatib-Ricaud-Desharnais-Tawbi-20] Souad El Hatib, Loïc Ricaud, Josée Desharnais, and Nadia Tawbi. "Toward Semantic-Based Android Malware Detection Using Model Checking". Proceedings of the 15th International Conference on Risks and Security of Internet and Systems (CRISIS'2020), Lecture Notes in Computer Science vol. 12528, pp. 289-307. Springer Verlag, November 2020. Available on-line at: https://doi.org/10.1007/978-3-030-68887-5_17 [ElHatib-20] Souad El Hatib. "Une approche sémantique de détection de maliciel Android basée sur la vérification de modèles et l'apprentissage automatique". MSc thesis, Laval University, Québec, Canada, 2020. Available on-line at: https://corpus.ulaval.ca/jspui/bitstream/20.500.11794/66322/1/36086.pdf or from the CADP Web site in PDF or PostScript
Contact:	Nadia Tawbi Département d'informatique et de génie logiciel Faculté des sciences et de génie 1065, avenue de la Médecine Université Laval Québec, (Qc), G1V 0A6 CANADA Email: Nadia.Tawbi@ift.ulaval.ca

Back to the CADP case studies page