Machine learning and formal methods for Android malware detection

The main focus of my PhD period is related to the detection of malware in the Android environment, using different techniques, so as to identify the threats to which the data saved on our devices are exposed. Everyday people use devices such as smartphones and tablets without thinking about problems related to their use, because smartphones handle a great deal of personal information (i.e., photos, finances, messages) that can be stolen. In fact, Android platform being the most popular mobile operating system, is also the most attacked by cybercriminals. The large popularity of Android combined with its open nature made this operating system a primary target of attackers able to develop more and more malicious apps at an industrial scale. From the defensive side, commercial and free antimalware software solutions are not able to correctly identify new threats, because the malicious payload is detectable only once its signature is stored in their repository. This context has been explored through three different steps: • The exploitation of the vulnerabilities present in the Android system; • the use of Machine Learning and Deep Learning techniques to detect the presence of malware, classify them according to malware families and analyze a new threat which takes the name of Colluding Attack; • the application of the Formal Methods technique for the analysis of the Colluding attack. The purpose of using different techniques is to explore their strengths and weaknesses. There are different vulnerabilities in the Android operating system, which can be exploited to launch attacks on the system and threaten our data. In this regard, some components of the smartphone have been used (i.e., the accelerometer and the vibration engine) as a covert channel to make the applications installed on the device communicate with each other, without the user's knowledge. A tool has been developed to inject malicious code into Android applications, thus making them collusive through the ExternalStorage Android resource. To promote the development of new methods to counter new emerging threats, a new malware was designed and developed that acts dynamically for a few moments, then completely deleting its traces on the infected device. Subsequently, Machine Learning and Deep Learning techniques were used to carry out analyses and classifications regarding Android malware. In particular, this type of techniques have been used to detect the presence of malware in infected Android applications, classify them according to family and understand whether the applications analyzed are involved in a Collusive Attack. The last step concerns the use of Formal Methods in order to provide greater explainability and interpretation of the results obtained. With the definition and the application of a Formal Methods approach, I analyzed trusted and infected Android applications, in order to detect the presence of Collusion, providing transparency of the obtained results. I model applications as automata and, using model verification techniques, I check if an app communicates with other applications installed on the device and is involved or not in a collusive attack. The experimental analysis confirms the effectiveness of the proposed method in detecting the behavior of applications, analyzing their data flow, obtaining good results compared to the previously mentioned approaches, which appear to be less precise.

Il focus principale del mio periodo di dottorato è legato al rilevamento di malware in ambiente Android, utilizzando diverse tecniche, in modo da identificare le minacce a cui sono esposti i dati salvati sui nostri dispositivi. Le persone comuni usano dispositivi come smartphone e tablet senza pensare ai problemi legati al loro utilizzo, perché gli smartphone gestiscono una grande quantità di informazioni personali (ad esempio foto, finanze, messaggi) che possono essere rubate. Infatti, essendo la piattaforma Android il sistema operativo mobile più popolare, è anche la più attaccata dai cybercriminali. La grande popolarità di Android unita alla sua natura aperta ha reso questo sistema operativo un obiettivo primario di aggressori in grado di sviluppare sempre più app dannose su scala industriale. Dal punto di vista difensivo, le soluzioni software antimalware commerciali e gratuite non sono in grado di identificare correttamente le nuove minacce, perché il payload dannoso è rilevabile solo una volta che la sua signature è stata memorizzata nel loro repository. Questo contesto è stato esplorato attraverso tre diverse fasi: • Lo sfruttamento delle vulnerabilità presenti nel sistema Android; • l'utilizzo di tecniche di Machine Learning e Deep Learning per rilevare la presenza di malware, classificarli per famiglie di malware e analizzare una nuova minaccia che prende il nome di Colluding Attack; • l'applicazione della tecnica dei Metodi Formali per l'analisi dell'attacco collusivo. Lo scopo dell'utilizzo di diverse tecniche è quello di esplorare i loro punti di forza e di debolezza. Esistono diverse vulnerabilità nel sistema operativo Android, che possono essere sfruttate per lanciare attacchi al sistema e minacciare i nostri dati. A tal proposito, alcuni componenti dello smartphone sono stati utilizzati (ovvero l'accelerometro e il motore di vibrazione) come canale occulto per far comunicare tra loro le applicazioni installate sul dispositivo, all'insaputa dell'utente. È stato sviluppato uno strumento per iniettare codice dannoso nelle applicazioni Android, rendendole così collusive tramite la risorsa Android dell’ExternalStorage. Per favorire lo sviluppo di nuovi metodi per contrastare le nuove minacce emergenti, è stato progettato e sviluppato un nuovo malware che agisce dinamicamente per alcuni istanti, cancellando poi completamente le sue tracce sul dispositivo infetto. Successivamente sono state utilizzate tecniche di Machine Learning e Deep Learning per effettuare analisi e classificazioni relative ai malware Android. In particolare, questo tipo di tecniche sono state utilizzate per rilevare la presenza di malware nelle applicazioni Android infette, classificarle per famiglia e capire se le applicazioni analizzate sono coinvolte in un attacco di Collusione. L'ultimo passaggio riguarda l'utilizzo dei Metodi Formali al fine di fornire una maggiore spiegabilità e interpretazione dei risultati ottenuti. Con la definizione e l'applicazione di un approccio di metodi formali, ho analizzato applicazioni Android attendibili e infette, al fine di rilevare la presenza di collusione, fornendo trasparenza dei risultati ottenuti. Modello le applicazioni come automi e, utilizzando tecniche di verifica del modello, controllo se un'app comunica con altre applicazioni installate sul dispositivo ed è coinvolta o meno in un attacco collusivo. L'analisi sperimentale conferma l'efficacia del metodo proposto nel rilevare il comportamento delle applicazioni, analizzando il loro flusso di dati, ottenendo buoni risultati rispetto agli approcci precedentemente citati, che appaiono meno precisi.