Talk "Software Model Checking for Mobile Security - Collusion Detection in K"

by Markus Roggenbach

Thu, 05 July 2018 at 02:00 pm in Royal Holloway, United Kingdom

Joint work with: Irina Asavoae, Hoang Nga Nguyen

Abstract: Cyber-security witnesses an ongoing expansion in various fields of research. This is due to the booming of cyber-physical systems and the necessity of evaluating and certifying their sustainability more efficiently. For example, until now security industry leaders, such as Intel Security, focused on malware analysis of only single applications. However, due to the highly collaborative app environment proposed by Android, the security evaluation needs to have more complex settings. This tutorial aims to define this security problem and to show how model checking can solve and/or alleviate it. Namely, we first focus on describing collusion–the property of an apps group of working together for producing malware. Secondly, we evaluate the exposure degree of the Android environment to the collusion problem. Thirdly, we present our proposal of employing model checking for collusion evaluation and the related work in formal methods for Android security. Finally, we discuss our view for future challenges and perspectives of formal methods in cybersecurity.