A Model Checking-based Approach to Malicious Family Detection in iOS Environment

As a result of the spread in the mobile market, new kinds of malware have developed. Many malicious users began to produce harmful applications for open-source operating systems such as Android, and closed-source operating systems like iOS. For this reason, new anti-malware methodologies are necessary to identify them. Currently, most of them base their approach on the signature, and it does not allow users to defend themselves from current threats. In this article, we propose an automatic tool able to identify dangerous iOS applications by defining a system model through Milner's Calculus of Communicating Systems and the consequence use of the State Transitions System to evaluate the behaviors of an application, to categorize if it is malware or a legitimate application. As a result of the experiments conducted, we obtained relevant performances with good precision and recall levels.